norm

Mathlib.Topology.Algebra.InfiniteSum.Field

URI: https://scilib.ai/kg/mathlib#HasProd.norm

English

If HasProd f x holds, then HasProd the normed sequence ‖f‖ has value ‖x‖.

Русский

Если HasProd f x, то HasProd нормы последовательности ‖f‖ равна ‖x‖.

LaTeX

$$HasProd f x → HasProd (\u2225f\u22c5) (\u2225x\u2225)$$

Lean4

nonrec theorem norm (hfx : HasProd f x) : HasProd (‖f ·‖) ‖x‖ :=
  by
  simp only [HasProd, ← norm_prod]
  exact hfx.norm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru