opNNNorm_le_bound' — Mathlib

English

If for all x with ‖x‖₊ ≠ 0 we have ‖f x‖₊ ≤ M‖x‖₊, then ‖f‖₊ ≤ M.

Русский

Если для всех x с ‖x‖₊ ≠ 0 выполняется ‖f x‖₊ ≤ M‖x‖₊, то ‖f‖₊ ≤ M.

LaTeX

$$$\\|f\\|_{+} \\le M$ assuming $\\forall x, \\|x\\|_{+} \\neq 0 \\rightarrow \\|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 opNNNorm_le_bound' (f : E →SL[σ₁₂] F) (M : ℝ≥0) (hM : ∀ x, ‖x‖₊ ≠ 0 → ‖f x‖₊ ≤ M * ‖x‖₊) : ‖f‖₊ ≤ M :=
  opNorm_le_bound' f (zero_le M) fun x hx => hM x <| by rwa [← NNReal.coe_ne_zero]

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