English
From an order isomorphism e: α ≃o β between lattices α and β, construct a lattice isomorphism α ≅ β with forward map ofHom e and inverse map ofHom e.symm.
Русский
Изоморфизм порядка e: α ≃o β между латами α и β порождает изоморфизм решеток α ≅ β, где отображение-строгость равняется ofHom e, а обратное отображение — ofHom e.symm.
LaTeX
$$$ \alpha \cong \beta \quad\text{with } \mathrm{hom} = \mathrm{ofHom}(e),\ \mathrm{inv} = \mathrm{ofHom}(e^{-1}). $$$
Lean4
/-- Constructs an isomorphism of lattices from an order isomorphism between them. -/
@[simps]
def mk {α β : Lat.{u}} (e : α ≃o β) : α ≅ β where
hom := ofHom e
inv := ofHom e.symm
