instProdNormedSpace — Mathlib

English

The product WithLp p (α × β) carries a natural NormedSpace structure provided α and β are normed spaces and p defines an appropriate lp-norm.

Русский

Произведение WithLp p (α × β) имеет естественную структуру нормированного пространства, если α и β нормированы и p задаёт подходящую lp-норму.

LaTeX

$$$\text{WithLp } p (\alpha \times \beta) \text{ is a NormedSpace if } α,β \text{ are NormedSpaces and } p \text{ is appropriate.}$$$

Lean4

/-- The product of two normed spaces is a normed space, with the `L^p` norm. -/
instance instProdNormedSpace [NormedField 𝕜] [NormedSpace 𝕜 α] [NormedSpace 𝕜 β] : NormedSpace 𝕜 (WithLp p (α × β))
    where norm_smul_le := norm_smul_le

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