opNorm_le_bound' — Mathlib

English

A variant bound: if ∥f x∥ ≤ M ∥x∥ whenever x ≠ 0, then ∥f∥ ≤ M.

Русский

Вариант границы: если ∥f x∥ ≤ M ∥x∥ при x ≠ 0, то ∥f∥ ≤ M.

LaTeX

$$$\\|f\\| \\le M \\quad\\text{если } \\forall x \\neq 0, \\|f x\\| \\le M \\|x\\|$$$

Lean4

/-- If one controls the norm of every `A x`, `‖x‖ ≠ 0`, then one controls the norm of `A`. -/
theorem opNorm_le_bound' (f : E →SL[σ₁₂] F) {M : ℝ} (hMp : 0 ≤ M) (hM : ∀ x, ‖x‖ ≠ 0 → ‖f x‖ ≤ M * ‖x‖) : ‖f‖ ≤ M :=
  opNorm_le_bound f hMp fun x =>
    (ne_or_eq ‖x‖ 0).elim (hM x) fun h => by simp only [h, mul_zero, norm_image_of_norm_zero f f.2 h, le_refl]

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