opNorm_comp_le — Mathlib

English

The operator norm is submultiplicative with respect to composition: the norm of h ∘ f is at most the product of the norms ‖h‖ and ‖f‖.

Русский

Норма оператора субпроизведение относительно композиции: норма h ∘ f не превышает произведение норм ‖h‖ и ‖f‖.

LaTeX

$$$ \|h \circ f\| \le \|h\| \cdot \|f\| $$$

Lean4

/-- The operator norm is submultiplicative. -/
theorem opNorm_comp_le (f : E →SL[σ₁₂] F) : ‖h.comp f‖ ≤ ‖h‖ * ‖f‖ :=
  csInf_le bounds_bddBelow
    ⟨by positivity, fun x => by
      rw [mul_assoc]
      exact h.le_opNorm_of_le (f.le_opNorm x)⟩

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