opNorm_le_bound — Mathlib

English

If a bound M ≥ 0 satisfies ∥f x∥ ≤ M ∥x∥ for all x, then ∥f∥ ≤ M.

Русский

Если существует граница M ≥ 0 такая, что ∥f x∥ ≤ M ∥x∥ для всех x, то ∥f∥ ≤ M.

LaTeX

$$$\\|f\\| \\le M \\quad\\text{if } M \\ge 0 \\text{ and } \\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 opNorm_le_bound (f : E →SL[σ₁₂] F) {M : ℝ} (hMp : 0 ≤ M) (hM : ∀ x, ‖f x‖ ≤ M * ‖x‖) : ‖f‖ ≤ M :=
  csInf_le bounds_bddBelow ⟨hMp, hM⟩

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