English
A simple bounded order has the structure of a complete Boolean algebra.
Русский
Простой ограниченный порядок обладает структурой полной булевой алгебры.
LaTeX
$$$\text{IsSimpleOrder.completeBooleanAlgebra}(\alpha)$$$
Lean4
/-- A simple `BoundedOrder` is also complete. -/
protected noncomputable def completeLattice : CompleteLattice α :=
{ (inferInstance : Lattice α),
(inferInstance : BoundedOrder α) with
sSup := fun s => if ⊤ ∈ s then ⊤ else ⊥
sInf := fun s => if ⊥ ∈ s then ⊥ else ⊤
le_sSup := fun s x h => by
rcases eq_bot_or_eq_top x with (rfl | rfl)
· exact bot_le
· rw [if_pos h]
sSup_le := fun s x h => by
rcases eq_bot_or_eq_top x with (rfl | rfl)
· rw [if_neg]
intro con
exact bot_ne_top (eq_top_iff.2 (h ⊤ con))
· exact le_top
sInf_le := fun s x h => by
rcases eq_bot_or_eq_top x with (rfl | rfl)
· rw [if_pos h]
· exact le_top
le_sInf := fun s x h => by
rcases eq_bot_or_eq_top x with (rfl | rfl)
· exact bot_le
· rw [if_neg]
intro con
exact top_ne_bot (eq_bot_iff.2 (h ⊥ con)) }
