norm_prod — Mathlib

English

For a finite index set s and a function f: s → ℂ, the norm of the product equals the product of norms: ‖s.prod f‖ = ∏ i∈s ‖f i‖.

Русский

Для конечного индекса s и функции f: s → ℂ выполняется: ‖(prod f)‖ = prod ‖f i‖.

LaTeX

$$$\|\prod_{i\in s} f(i)\| = \prod_{i\in s} \|f(i)\|$$$

Lean4

protected theorem norm_prod {ι : Type*} (s : Finset ι) (f : ι → ℂ) : ‖s.prod f‖ = s.prod fun i ↦ ‖f i‖ :=
  map_prod isAbsoluteValueNorm.abvHom _ _

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