Power_Set_is_Complete_Lattice
Provedlattice-theorypower-setproofwiki
The power set of S ordered by subset inclusion is a complete lattice: every collection of subsets has a greatest lower bound.
Preamble
import Mathlib.Data.Set.Lattice import Mathlib.Order.Bounds.Basic
Formal statement
theorem Power_Set_is_Complete_Lattice {α : Type _} (S : Set (Set α)) : ∃ x : Set α, x ∈ lowerBounds S ∧ ∀ y ∈ lowerBounds S, y ⊆ x := by sorrySource