nnnorm_prod — Mathlib

English

For a finite set s and a function f: s → α, the NNReal norm of the finite product equals the product of NNReal norms.

Русский

Для конечного множества s и функции f: s → α, NNReal-норма произведения равна произведению NNReal-норм элементов.

LaTeX

$$$\\|\\prod_{b\\in s} f(b)\\|_{+} = \\prod_{b\\in s} \\|f(b)\\|_{+}$$$

Lean4

@[simp]
theorem nnnorm_prod (s : Finset β) (f : β → α) : ‖∏ b ∈ s, f b‖₊ = ∏ b ∈ s, ‖f b‖₊ :=
  map_prod nnnormHom.toMonoidHom f s

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