English
A distributive lattice that is complemented can be given a Boolean algebra structure.
Русский
Дистрибутивная решётка, имеющая дополнение, может быть наделена структурой булевой алгебры.
LaTeX
$$$[\text{DistribLattice}(\alpha)] \wedge [\text{BoundedOrder}(\alpha)] \wedge [\text{ComplementedLattice}(\alpha)] \Rightarrow [\text{BooleanAlgebra}(\alpha)].$$$
Lean4
/-- An alternative constructor for Boolean algebras:
a distributive lattice that is complemented is a Boolean algebra.
This is not an instance, because it creates data using choice.
-/
noncomputable def booleanAlgebraOfComplemented [BoundedOrder α] [ComplementedLattice α] : BooleanAlgebra α
where
__ := (inferInstanceAs (BoundedOrder α))
compl a := Classical.choose <| exists_isCompl a
inf_compl_le_bot a := (Classical.choose_spec (exists_isCompl a)).disjoint.le_bot
top_le_sup_compl a := (Classical.choose_spec (exists_isCompl a)).codisjoint.top_le
