ext

Mathlib.Analysis.Normed.Group.SemiNormedGrp

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

English

Two morphisms in SemiNormedGrp₁ are equal if they have the same underlying hom.

Русский

Два морфизма в SemiNormedGrp₁ равны, если они имеют одинаковый подлежащий гомоморфизм.

LaTeX

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

Lean4

@[ext]
theorem ext {M N : SemiNormedGrp₁} {f₁ f₂ : M ⟶ N} (h : ∀ (x : M), f₁ x = f₂ x) : f₁ = f₂ :=
  ConcreteCategory.ext_apply h

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

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

Разделы

Аффилиация

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