normedAddCommGroup — Mathlib

English

If each β_i is a normed additive commutative group, then the Lp-product PiLp p β is a NormedAddCommGroup (with the Lp-norm).

Русский

Если для каждого i множество β_i образует нормированную аддитивно-коммутативную группу, то произведение PiLp p β с нормой L^p является нормированной аддитивной группой.

LaTeX

$$$$ \operatorname{NormedAddCommGroup}(\PiLp\,p\,\beta) $$$$

Lean4

/-- normed group instance on the product of finitely many normed groups, using the `L^p` norm. -/
instance normedAddCommGroup [∀ i, NormedAddCommGroup (α i)] : NormedAddCommGroup (PiLp p α) :=
  { PiLp.seminormedAddCommGroup p α with eq_of_dist_eq_zero := eq_of_dist_eq_zero }

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