English
A simple bounded order is a complete lattice.
Русский
Простой ограниченный порядок является полной решёткой.
LaTeX
$$$\text{IsSimpleOrder.completeLattice}(\alpha)$$$
Lean4
/-- A simple `BoundedOrder` is also a `BooleanAlgebra`. -/
protected def booleanAlgebra {α} [DecidableEq α] [Lattice α] [BoundedOrder α] [IsSimpleOrder α] : BooleanAlgebra α :=
{ inferInstanceAs (BoundedOrder α),
IsSimpleOrder.distribLattice with
compl := fun x => if x = ⊥ then ⊤ else ⊥
sdiff := fun x y => if x = ⊤ ∧ y = ⊥ then ⊤ else ⊥
sdiff_eq := fun x y => by rcases eq_bot_or_eq_top x with (rfl | rfl) <;> simp
inf_compl_le_bot := fun x => by
rcases eq_bot_or_eq_top x with (rfl | rfl)
· simp
· simp
top_le_sup_compl := fun x => by rcases eq_bot_or_eq_top x with (rfl | rfl) <;> simp }
