English
There exists an order isomorphism between AsBoolAlg (AsBoolRing α) and α, given by the composition of the standard maps ofBoolAlg and ofBoolRing.
Русский
Существует упорядоченная изоморфия между AsBoolAlg (AsBoolRing α) и α, задаваемая композициями соответствующих карт.
LaTeX
$$$\text{There exists an order isomorphism } AsBoolAlg(AsBoolRing(α)) \simeq_o α \;\text{ with the explicit maps }\text{ofBoolAlg}, \text{ofBoolRing}. $$$
Lean4
/-- Order isomorphism between `α` considered as a Boolean ring considered as a Boolean algebra and
`α`. -/
@[simps!]
def asBoolAlgAsBoolRing (α : Type*) [BooleanAlgebra α] : AsBoolAlg (AsBoolRing α) ≃o α :=
⟨ofBoolAlg.trans ofBoolRing, ofBoolRing_le_ofBoolRing_iff.trans ofBoolAlg_mul_ofBoolAlg_eq_left_iff⟩
