@[simp]

theorem Set.greatest_iff_univ {α : Type u_1} {x : Set α} : Greatest x ↔ x = Set.univ

@[simp]

theorem Set.least_iff_empty {α : Type u_1} {x : Set α} : Least x ↔ x = ∅

theorem Set.minimal_iff_singleton_nonempty {α : Type u_1} {x : { x : Set α // x.Nonempty }} : Minimal x ↔ ∃ (a : α), x = ⟨{a}, ⋯⟩

theorem Set.intersection_least_of_mem {α : Type u_1} {p : Set α → Prop} (h : p (⋂ a : { x : Set α // p x }, a.val)) : Least ⟨⋂ a : { x : Set α // p x }, a.val, h⟩

theorem Set.union_greatest_of_mem {α : Type u_1} {p : Set α → Prop} (h : p (⋃ a : { x : Set α // p x }, a.val)) : Greatest ⟨⋃ a : { x : Set α // p x }, a.val, h⟩

theorem Set.least_eq_intersection {α : Type u_1} {p : Set α → Prop} {x : { x : Set α // p x }} (h : Least x) : x.val = ⋂ a : { x : Set α // p x }, a.val

theorem Set.greatest_eq_union {α : Type u_1} {p : Set α → Prop} {x : { x : Set α // p x }} (h : Greatest x) : x.val = ⋃ a : { x : Set α // p x }, a.val

@[simp]

theorem Set.iInter_isGLB {α : Type u_1} {s : Set (Set α)} : IsGLB s (⋂ a : ↥s, a.val)

@[simp]

theorem Set.iUnion_isLUB {α : Type u_1} {s : Set (Set α)} : IsLUB s (⋃ a : ↥s, a.val)

noncomputable instance Set.instHasLeast {α : Type u_1} : HasLeast (Set α)

Equations

• Set.instHasLeast = { least := ∅, least_le := ⋯ }

noncomputable instance Set.instHasGreatest {α : Type u_1} : HasGreatest (Set α)

Equations

• Set.instHasGreatest = { greatest := Set.univ, le_greatest := ⋯ }

@[simp]

theorem Set.least_eq {α : Type u_1} : ⊥ = ∅

@[simp]

theorem Set.greatest_eq {α : Type u_1} : ⊤ = Set.univ