ext

Mathlib.Analysis.Normed.Group.SemiNormedGrp

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

English

Two morphisms in SemiNormedGrp are equal if they agree on every element of the source.

Русский

Два морфизмa в SemiNormedGrp равны, если они совпадают на каждом элементе источника.

LaTeX

$$$ \forall x : M,\ f_1 x = f_2 x \Rightarrow f_1 = f_2 $$$

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