norm_comp_le_of_le — Mathlib

English

Let f: V1 → V2 and g: V2 → V3 be normed maps with norms ||f|| ≤ C1 and ||g|| ≤ C2. Then ||g ∘ f|| ≤ C2 · C1.

Русский

Пусть f: V1 → V2 и g: V2 → V3 такие, что ||f|| ≤ C1, ||g|| ≤ C2. Тогда ||g ∘ f|| ≤ C2 · C1.

LaTeX

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

Lean4

theorem norm_comp_le_of_le {g : NormedAddGroupHom V₂ V₃} {C₁ C₂ : ℝ} (hg : ‖g‖ ≤ C₂) (hf : ‖f‖ ≤ C₁) :
    ‖g.comp f‖ ≤ C₂ * C₁ :=
  le_trans (norm_comp_le g f) <| by gcongr; exact le_trans (norm_nonneg _) hg

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