nnnorm_eq_ciSup — Mathlib

English

For f in PiLp ∞ β, the NN-norm equals the supremum of the coordinate NN-norms: ‖f‖₊ = ⨆ i, ‖f_i‖₊.

Русский

Для f ∈ PiLp ∞ β нормa NN равна супремуму норм координат: ‖f‖₊ = ⨆_i ‖f_i‖₊.

LaTeX

$$$$ \|f\|_{+} = \big\lVert \{ \|f_i\|_{+} : i \in \iota \} \big\rVert_{\infty} = \bigvee_i \|f_i\|_{+} $$$$

Lean4

theorem nnnorm_eq_ciSup (f : PiLp ∞ β) : ‖f‖₊ = ⨆ i, ‖f i‖₊ :=
  by
  ext
  simp [NNReal.coe_iSup, norm_eq_ciSup]

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