equivLike — Mathlib

English

ContinuousAlgEquiv carries an EquivLike structure, i.e., it behaves like an equivalence with fun-like coercions.

Русский

ContinuousAlgEquiv обладает структурой EquivLike, то есть ведёт себя как эквивалентность с приведением по функции.

LaTeX

$$EquivLike(ContinuousAlgEquiv R A B) A B$$

Lean4

instance equivLike : EquivLike (A ≃A[R] B) A B where
  coe f := f.toFun
  inv f := f.invFun
  coe_injective' f g h₁
    h₂ := by
    obtain ⟨f', _⟩ := f
    obtain ⟨g', _⟩ := g
    rcases f' with ⟨⟨_, _⟩, _⟩
    rcases g' with ⟨⟨_, _⟩, _⟩
    congr
  left_inv f := f.left_inv
  right_inv f := f.right_inv

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