opNNNorm_le_bound — Mathlib

English

If for every x we have ‖f x‖ ≤ M‖x‖ with M ≥ 0, then ‖f‖ ≤ M.

Русский

Если для каждого x выполняется ‖f x‖ ≤ M‖x‖, тогда ‖f‖ ≤ M.

LaTeX

$$$\\|f\\|_{+} \\le M$ assuming $\\forall x, \\|f x\\|_{+} \\le M \\|x\\|_{+}$$$

Lean4

/-- If one controls the norm of every `A x`, then one controls the norm of `A`. -/
theorem opNNNorm_le_bound (f : E →SL[σ₁₂] F) (M : ℝ≥0) (hM : ∀ x, ‖f x‖₊ ≤ M * ‖x‖₊) : ‖f‖₊ ≤ M :=
  opNorm_le_bound f (zero_le M) hM

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