norm_comp_le_of_le' — Mathlib

English

Let f: V1 → V2 and g: V2 → V3 with constants C1, C2, C3 such that C3 = C2 · C1 and ||g|| ≤ C2, ||f|| ≤ C1. Then ||g ∘ f|| ≤ C3.

Русский

Пусть C3 = C2 · C1 и ||g|| ≤ C2, ||f|| ≤ C1. Тогда ||g ∘ f|| ≤ C3.

LaTeX

$$$\\| g \\circ f \\| \\leq C_3 \\quad\\text{где}\\quad C_3 = C_2 C_1$$$

Lean4

theorem norm_comp_le_of_le' {g : NormedAddGroupHom V₂ V₃} (C₁ C₂ C₃ : ℝ) (h : C₃ = C₂ * C₁) (hg : ‖g‖ ≤ C₂)
    (hf : ‖f‖ ≤ C₁) : ‖g.comp f‖ ≤ C₃ := by
  rw [h]
  exact norm_comp_le_of_le hg hf

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