norm_comp_le — Mathlib

English

Let f: V1 → V2 and g: V2 → V3 be normed additive group homomorphisms. Then the operator norm of their composition does not exceed the product of their operator norms: ||g ∘ f|| ≤ ||g|| · ||f||.

Русский

Пусть f: V1 → V2 и g: V2 → V3 — гомоморфизмы нормированных аддитивных групп. Тогда нормa оператора композиции удовлетворяет: ||g ∘ f|| ≤ ||g|| · ||f||.

LaTeX

$$$\\| g \\circ f \\| \\leq \\|g\\| \\cdot \\|f\\|$$$

Lean4

theorem norm_comp_le (g : NormedAddGroupHom V₂ V₃) (f : NormedAddGroupHom V₁ V₂) : ‖g.comp f‖ ≤ ‖g‖ * ‖f‖ :=
  mkNormedAddGroupHom_norm_le _ (by positivity) _

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