abs_tprod — Mathlib

English

The absolute value of an infinite product equals the infinite product of absolute values: |∏' i, f i| = ∏' i, |f i|.

Русский

Модуль бесконечного произведения совпадает с бесконечным произведением модулей: |∏' i, f i| = ∏' i, |f i|.

LaTeX

$$$$\\left| \\prod' i, f i \\right| = \\prod' i, |f i|.$$$$

Lean4

protected theorem abs_tprod (hf : Multipliable f) : |∏' i, f i| = ∏' i, |f i| :=
  hf.hasProd.abs.tprod_eq.symm

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