norm_def — Mathlib

English

Let f be a continuous alternating multilinear map f: E [⋀^ι]→L[𝕜] F. Then the operator norm of f equals the infimum of all nonnegative numbers c such that for every input m : ι → E, one has ‖f m‖ ≤ c · ∏ i, ‖m i‖.

Русский

Пусть f — непрерывное чередующее мультилинейное отображение f: E [⋀^ι]→L[𝕜] F. Тогда операторная норма f равна наименьшему неотрицательному числу c, для которого для всякого входа m : ι → E выполняется ‖f m‖ ≤ c · ∏ i, ‖m i‖.

LaTeX

$$$$\|f\| = \inf\{c \in \mathbb{R} : 0 \le c \wedge \forall m, \|f m\| \le c \prod_{i \in \iota} \|m_i\|\}$$$$

Lean4

theorem norm_def (f : E [⋀^ι]→L[𝕜] F) : ‖f‖ = sInf {c : ℝ | 0 ≤ c ∧ ∀ m, ‖f m‖ ≤ c * ∏ i, ‖m i‖} :=
  rfl

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