mk — Mathlib · SciLib

English

From an order isomorphism e between two bounded lattices, construct an isomorphism of the corresponding bounded lattices.

Русский

По порядкoму изоморфизму e между двумя ограниченными решетками строится изоморфизм соответствующих ограниченных решеток.

LaTeX

$$def mk {α β : BddLat.{u}} (e : α ≃o β) : α ≅ β$$

Lean4

/-- Constructs an equivalence between bounded lattices from an order isomorphism
between them. -/
@[simps]
def mk {α β : BddLat.{u}} (e : α ≃o β) : α ≅ β where
  hom := ofHom e
  inv := ofHom e.symm
  hom_inv_id := by ext; exact e.symm_apply_apply _
  inv_hom_id := by ext; exact e.apply_symm_apply _

Похожие утверждения