opNorm_smul_le — Mathlib

English

For any scalar c and any continuous linear map f, the operator norm of the scaled map c f is at most the product of |c| and the operator norm of f.

Русский

Для любого скаляра c и любого непрерывно линейного отображения f норма оператора отображения c f не превышает произведение |c| и нормы f.

LaTeX

$$$ \|c \cdot f\| \le \|c\| \cdot \|f\| $$$

Lean4

theorem opNorm_smul_le {𝕜' : Type*} [NormedField 𝕜'] [NormedSpace 𝕜' F] [SMulCommClass 𝕜₂ 𝕜' F] (c : 𝕜')
    (f : E →SL[σ₁₂] F) : ‖c • f‖ ≤ ‖c‖ * ‖f‖ :=
  (c • f).opNorm_le_bound (mul_nonneg (norm_nonneg _) (opNorm_nonneg _)) fun _ =>
    by
    rw [smul_apply, norm_smul, mul_assoc]
    gcongr
    apply le_opNorm

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