normedSpace — Mathlib

English

The product of finitely many normed spaces is a normed space with sup norm.

Русский

Произведение конечного числа нормированных пространств является нормированным пространством с суп-нормой.

LaTeX

$$$\\|f\\| = \\sup_{i} \\|f(i)\\|$$$

Lean4

/-- The product of finitely many normed spaces is a normed space, with the sup norm. -/
instance normedSpace {ι : Type*} {E : ι → Type*} [Fintype ι] [∀ i, SeminormedAddCommGroup (E i)]
    [∀ i, NormedSpace 𝕜 (E i)] : NormedSpace 𝕜 (∀ i, E i) where
  norm_smul_le a
    f := by
    simp_rw [← coe_nnnorm, ← NNReal.coe_mul, NNReal.coe_le_coe, Pi.nnnorm_def, NNReal.mul_finset_sup]
    exact Finset.sup_mono_fun fun _ _ => norm_smul_le a _

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