norm_def — Mathlib

English

For a continuous linear map f between normed spaces, its operator norm is the smallest nonnegative real number M such that ∥f x∥ ≤ M ∥x∥ for every x.

Русский

Для непрерывного линейного отображения f между нормированными пространствами его операторная норма есть наименьшее неотрицательное число M такое, что ∥f x∥ ≤ M ∥x∥ для всех x.

LaTeX

$$$\\|f\\| = \\inf\\{ c \\in \\mathbb{R} \\mid 0 \\le c \\wedge \\forall x, \\|f x\\| \\le c \\|x\\| \\}$$$

Lean4

theorem norm_def (f : E →SL[σ₁₂] F) : ‖f‖ = sInf {c | 0 ≤ c ∧ ∀ x, ‖f x‖ ≤ c * ‖x‖} :=
  rfl

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