funLike — Mathlib

English

Two normed additive group homomorphisms are equal if their coe to functions are equal.

Русский

Два нормированных гомоморфизма равны тогда и только тогда, когда их отображение как функций совпадает.

LaTeX

$$$f=g \\iff (f:V_1\\to V_2)=(g)$$$

Lean4

instance funLike : FunLike (NormedAddGroupHom V₁ V₂) V₁ V₂
    where
  coe := toFun
  coe_injective' f g h := by cases f; cases g; congr

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