opNNNorm_pi — Mathlib

English

The NNReal norm of pi f equals the NNReal norm of f for a family f.

Русский

NNReal-норма pi f равна NNReal-норме f для семейства f.

LaTeX

$$$$\|\pi f\|_{+} = \|f\|_{+}.$$$$

Lean4

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

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