normedGroup — Mathlib

English

If each G_i is a NormedGroup and ι is finite, then the product ∏_i G_i, with the sup-norm, is a NormedGroup.

Русский

Если каждый G_i — нормированная группа, то их конечное произведение оборудовано нормой и является NormedGroup.

LaTeX

$$Finite product of normed groups, using the sup norm.$$

Lean4

/-- Finite product of normed groups, using the sup norm. -/
@[to_additive /-- Finite product of seminormed groups, using the sup norm. -/
    ]
instance normedGroup [∀ i, NormedGroup (G i)] : NormedGroup (∀ i, G i) :=
  { Pi.seminormedGroup with eq_of_dist_eq_zero := eq_of_dist_eq_zero }

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