instNormedSpace — Mathlib

English

For p ≥ 1, the Lp(E,p,μ) space carries a norm making it a normed space over 𝕜; the norm agrees with the underlying Lp-norm and respects scalar multiplication.

Русский

Для p ≥ 1 пространство Lp(E,p,μ) имеет норму, делающую его нормированным пространством над 𝕜; норма согласована с Lp-нормой и уважает умножение скаляров.

LaTeX

$$$NormedSpace\ 𝕜\ (Lp\ E\ p\ μ)$$$

Lean4

instance instNormedSpace [Fact (1 ≤ p)] : NormedSpace 𝕜 (Lp E p μ) where norm_smul_le _ _ := norm_smul_le _ _

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