English
Let p be a real ENNReal with 1 ≤ p and β_i be normed spaces over a field 𝕜, indexed by a finite set ι. Then the finite product space ∏_{i∈ι} β_i, equipped with the L^p norm, is a normed space over 𝕜.
Русский
Пусть p—положительная величина в Лемме ENNReal с 1 ≤ p, а β_i — нормированные пространства над полем 𝕜, индексированные конечным множеством ι. Тогда конечное произведение ∏_{i∈ι} β_i, наделённое нормой L^p, образует нормированное пространство над 𝕜.
LaTeX
$$$\operatorname{NormedSpace}_{\mathbb{K}}\bigl(\Pi_{i \in \iota} \beta_i\bigr)\quad\text{with the }L^p\text{-norm}$$
Lean4
/-- The product of finitely many normed spaces is a normed space, with the `L^p` norm. -/
instance normedSpace [NormedField 𝕜] [∀ i, SeminormedAddCommGroup (β i)] [∀ i, NormedSpace 𝕜 (β i)] :
NormedSpace 𝕜 (PiLp p β) where norm_smul_le := norm_smul_le
