opNorm_pi — Mathlib

English

The operator norm of the pi-map equals the operator norm of the family of maps.

Русский

Операторная норма карты pi равна операторной норме семейства отображений.

LaTeX

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

Lean4

theorem opNorm_pi {ι' : Type*} [Fintype ι'] {F : ι' → Type*} [∀ i', SeminormedAddCommGroup (F i')]
    [∀ i', NormedSpace 𝕜 (F i')] (f : ∀ i', E [⋀^ι]→L[𝕜] F i') : ‖pi f‖ = ‖f‖ :=
  ContinuousMultilinearMap.opNorm_pi fun i ↦ (f i).1

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