instNormedAddTorsorProd — Mathlib

English

There is a natural NormedAddTorsor structure on the product V × W with P × Q, aligning the product norms with coordinate norms.

Русский

Существует естественная структура NormedAddTorsor на произведении V × W с P × Q, согласующая норму произведения с нормами координат.

LaTeX

$$NormedAddTorsor (Prod V W) (Prod P Q)$$

Lean4

instance : NormedAddTorsor (V × W) (P × Q) where
  dist_eq_norm' x
    y := by simp only [Prod.dist_eq, NormedAddTorsor.dist_eq_norm', Prod.norm_def, Prod.fst_vsub, Prod.snd_vsub]

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