normedSpace — Mathlib

English

The finitely-indexed product of normed spaces is a normed space with the sup norm.

Русский

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

LaTeX

$$$\\|f\\|_{\\infty} = \\max_{i \\in ι} \\|f(i)\\|$ for finitely many i$$

Lean4

/-- The product of two normed spaces is a normed space, with the sup norm. -/
instance normedSpace : NormedSpace 𝕜 (E × F) :=
  { Prod.seminormedAddCommGroup (E := E) (F := F), Prod.instModule with
    norm_smul_le := fun s x => by simp only [norm_smul, Prod.norm_def, mul_max_of_nonneg, norm_nonneg, le_rfl] }

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