opNorm_le_iff — Mathlib

English

For any M ≥ 0, ∥f∥ ≤ M if and only if ∥f x∥ ≤ M ∥x∥ for all x.

Русский

Для любого M ≥ 0 верно: ∥f∥ ≤ M тогда и только тогда, когда ∥f x∥ ≤ M ∥x∥ для всех x.

LaTeX

$$$\\|f\\| \\le M \\iff \\forall x, \\|f x\\| \\le M \\|x\\|$$$

Lean4

theorem opNorm_le_iff {f : E →SL[σ₁₂] F} {M : ℝ} (hMp : 0 ≤ M) : ‖f‖ ≤ M ↔ ∀ x, ‖f x‖ ≤ M * ‖x‖ :=
  ⟨f.le_of_opNorm_le, opNorm_le_bound f hMp⟩

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