English
From an order isomorphism e: α ≃o β between bounded lattices α and β, one obtains an isomorphism α ≅ β in the category BddDistLat, with hom := ofHom e and inv := ofHom e.symm.
Русский
Из упорядоченного изоморфизма e: α ≃o β между уравновешенными распределительными решётками строится изоморфизм α ≅ β в категории BddDistLat, причём отображение-односторонняя стрелка задаются как ofHom e и его обратное как ofHom e.symm.
LaTeX
$$$ mk(e) : \alpha \cong \beta \quad\text{with}\quad \mathrm{hom}=\mathrm{ofHom}(e), \mathrm{inv}=\mathrm{ofHom}(e.symm) $$$
Lean4
/-- Constructs an equivalence between bounded distributive lattices from an order isomorphism
between them. -/
@[simps]
def mk {α β : BddDistLat.{u}} (e : α ≃o β) : α ≅ β
where
hom := BddDistLat.ofHom e
inv := BddDistLat.ofHom e.symm
