English
From an order isomorphism e between complete lattices α and β, there is a corresponding isomorphism of complete lattices α ≅ β, with forward and inverse given by the induced lattice-homomorphisms.
Русский
Из ордер-изоморфизма e между полными решётками α и β следует изоморфизм полных решёток α ≅ β, тождественные отображения задаются соответствующими гомоморфизмами решёток.
LaTeX
$$$$ \exists I: \alpha \cong \beta. $$$$
Lean4
/-- Constructs an equivalence between Boolean algebras from an order isomorphism between them. -/
@[simps]
def mk {α β : BoolAlg.{u}} (e : α ≃o β) : α ≅ β where
hom := ofHom e
inv := ofHom e.symm
