toAddMonoidHom_injective — Mathlib

English

The map that sends a NormedAddGroupHom to its underlying AddMonoidHom is injective; i.e., if two normed morphisms have the same underlying monoid homomorphism, they are equal.

Русский

Отображение NormedAddGroupHom в его базовый AddMonoidHom инъективно; если два нормированых гомоморфизма имеют одинаковый базовый гомоморфизм, то они равны.

LaTeX

$$$\\forall f,g:\\ NormedAddGroupHom\\ V_1\\ V_2,\\ (f.toAddMonoidHom = g.toAddMonoidHom) \\Rightarrow f=g$$$

Lean4

theorem toAddMonoidHom_injective : Function.Injective (@NormedAddGroupHom.toAddMonoidHom V₁ V₂ _ _) := fun f g h =>
  coe_inj <| by rw [← coe_toAddMonoidHom f, ← coe_toAddMonoidHom g, h]

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