def Cofinal {α : Type u_1} [Preorder α] (s : Set α) : Prop

Equations

• Cofinal s = ∀ (x : α), ∃ (y : α), y ∈ s ∧ x ≤ y

def Coinitial {α : Type u_1} [Preorder α] (s : Set α) : Prop

Equations

• Coinitial s = ∀ (x : α), ∃ (y : α), y ∈ s ∧ y ≤ x

theorem singleton_cofinal_iff_greatest {α : Type u_1} [Preorder α] {a : α} : Cofinal {a} ↔ Greatest a

theorem singleton_coinitial_iff_least {α : Type u_1} [Preorder α] {a : α} : Coinitial {a} ↔ Least a

@[simp]

theorem Cofinal.univ {α : Type u_1} [Preorder α] : Cofinal Set.univ

theorem Cofinal.cofinal_of_subset {α : Type u_1} [Preorder α] {s t : Set α} (h : Cofinal s) (h' : s ⊆ t) : Cofinal t