smul — Mathlib

English

If f is a bounded linear map, so is -f.

Русский

Если f ограничено линейно отображение, то и -f ограничено линейно отображение.

LaTeX

$$$ \\text{IsBoundedLinearMap } 𝕜 ( - f ) $$$

Lean4

theorem smul (c : 𝕜) (hf : IsBoundedLinearMap 𝕜 f) : IsBoundedLinearMap 𝕜 (c • f) :=
  let ⟨hlf, M, _, hM⟩ := hf
  (c • hlf.mk' f).isLinear.with_bound (‖c‖ * M) fun x =>
    calc
      ‖c • f x‖ = ‖c‖ * ‖f x‖ := norm_smul c (f x)
      _ ≤ ‖c‖ * (M * ‖x‖) := (mul_le_mul_of_nonneg_left (hM _) (norm_nonneg _))
      _ = ‖c‖ * M * ‖x‖ := (mul_assoc _ _ _).symm

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