ι_normNoninc — Mathlib

English

Let E be the equalizer of two normed additive group homomorphisms f and g. The natural inclusion iota from E into the ambient group V does not increase norms; i.e., for every v in E, ||iota(v)|| ≤ ||v||.

Русский

Пусть E — равновесная подгруппа (эквалайзер) двух нормированных гомоморфизмов f и g. Включение iota: E → V не увеличивает норму, то есть для любого v ∈ E выполняется ||iota(v)|| ≤ ||v||.

LaTeX

$$$\| (\iota f g)\,v \| \le \| v \| \quad \text{для всех } v \\in \\mathrm{NormedAddGroupHom.Equalizer}(f,g).$$$

Lean4

theorem ι_normNoninc : (ι f g).NormNoninc := fun _v => le_rfl

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