instEquivLike — Mathlib

English

There is an EquivLike structure on OrderMonoidIso α β, providing a canonical notion of equivalences between ordered monoid isomorphisms.

Русский

Существует структура EquivLike на OrderMonoidIso α β, задающая каноническое понятие эквивалентностей между упорядоченными моноид-изоморфизмами.

LaTeX

$$EquivLike structure on OrderMonoidIso α β.$$

Lean4

@[to_additive]
instance : EquivLike (α ≃*o β) α β where
  coe f := f.toFun
  inv f := f.invFun
  left_inv f := f.left_inv
  right_inv f := f.right_inv
  coe_injective' f g h₁
    h₂ := by
    obtain ⟨⟨⟨_, _⟩⟩, _⟩ := f
    obtain ⟨⟨⟨_, _⟩⟩, _⟩ := g
    congr

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