mk — Mathlib · SciLib

English

For α Boolean algebra with Finite type, the carrier of FinBoolAlg.of α equals α.

Русский

Для α булевой алгебры с конечным множеством базового типа каркас FinBoolAlg.of α равен α.

LaTeX

$$$ (\\mathrm{FinBoolAlg}.of\\; \\alpha).\\mathrm{carrier} = \\alpha. $$$

Lean4

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

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