opNorm_pi — Mathlib

English

Let f be a family of continuous multilinear maps indexed by ι'. The operator norm of the product map π f equals the operator norm of f itself. This expresses that assembling the component maps into a single π-map does not change the overall operator bound.

Русский

Пусть f — семейство непрерывных многоилинейных отображений, индексируемых ι'. Нормa оператора произведённого отображения π f равна норме оператора исходного семейства f.

LaTeX

$$$\|\pi f\| = \|f\|$$$

Lean4

theorem opNorm_pi {ι' : Type v'} [Fintype ι'] {E' : ι' → Type wE'} [∀ i', SeminormedAddCommGroup (E' i')]
    [∀ i', NormedSpace 𝕜 (E' i')] (f : ∀ i', ContinuousMultilinearMap 𝕜 E (E' i')) : ‖pi f‖ = ‖f‖ :=
  congr_arg NNReal.toReal (opNNNorm_pi f)

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