norm_tprod

Mathlib.Topology.Algebra.InfiniteSum.Field

URI: https://scilib.ai/kg/mathlib#Multipliable.norm_tprod

English

The norm of the infinite product equals the product of the norms: ‖tprod f‖ = tprod ‖f‖.

Русский

Норма бесконечного произведения равна произведению норм: ‖tprod f‖ = tprod ‖f‖.

LaTeX

$$‖tprod f‖ = tprod (fun i => ‖f i‖)$$

Lean4

protected theorem norm_tprod (hf : Multipliable f) : ‖∏' i, f i‖ = ∏' i, ‖f i‖ :=
  hf.hasProd.norm.tprod_eq.symm

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

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

Разделы

Аффилиация

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