equivLike — Mathlib

English

Two continuous linear equivalences are equal if their underlying functions are equal; i.e., equality is determined pointwise.

Русский

Две непрерывные линейные эквивалентности равны, если их базовые отображения совпадают, т.е. равенство определяется по точкам.

LaTeX

$$$ f = g \iff (\forall x, f(x) = g(x)) $$$

Lean4

instance equivLike : EquivLike (M₁ ≃SL[σ₁₂] M₂) M₁ M₂
    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

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