hom_ext

Mathlib.Analysis.Normed.Group.SemiNormedGrp

URI: https://scilib.ai/kg/mathlib#SemiNormedGrp₁.hom_ext

English

If f.hom = g.hom, then f = g.

Русский

Если f.hom = g.hom, то f = g.

LaTeX

$$$ f.hom = g.hom \Rightarrow f = g $$$

Lean4

@[ext]
theorem hom_ext {M N : SemiNormedGrp₁} {f g : M ⟶ N} (hf : f.hom = g.hom) : f = g :=
  Hom.ext (congr_arg Subtype.val hf)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru