instEquivLike — Mathlib

English

The family AlgEquiv R A B carries an EquivLike structure, i.e., it behaves like a family of equivalences with a coherent coercion to functions.

Русский

Семейство AlgEquiv R A B имеет структуру EquivLike; это ведет себя как множество эквивалентностей с согласованной приводимостью к функциям.

LaTeX

$$EquivLike (AlgEquiv R A B) A B$$

Lean4

instance : EquivLike (A₁ ≃ₐ[R] A₂) A₁ A₂ 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, _⟩, _⟩ := f
    obtain ⟨⟨g, _⟩, _⟩ := g
    congr

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