English
From an order isomorphism e: α ≃o β one obtains a lattice isomorphism α ≅ β with hom := e and inv := e.symm.
Русский
Из порядочного изоморфизма e: α ≃o β получается решётко-изоморфизм α ≅ β с гомоморфизмом e и обратным e.symm.
LaTeX
$$$ \\alpha \\cong \\beta \\text{ with } \\mathrm{hom} = e, \\mathrm{inv} = e^{\\mathrm{symm}} $$$
Lean4
/-- Constructs an isomorphism of lattices from an order isomorphism between them. -/
@[simps]
def mk {α β : SemilatInfCat.{u}} (e : α ≃o β) : α ≅ β
where
hom := (e : InfTopHom _ _)
inv := (e.symm : InfTopHom _ _)
hom_inv_id := by ext; exact e.symm_apply_apply _
inv_hom_id := by ext; exact e.apply_symm_apply _
