norm_prod — Mathlib

English

For a finite set s and a function f from the set to α, the norm of the product ∏_{b∈s} f(b) equals the product of the norms ∏_{b∈s} ‖f(b)‖.

Русский

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

LaTeX

$$$\\left\\|\\prod_{b\\in s} f(b)\\right\\| = \\prod_{b\\in s} \\|f(b)\\|$$$

Lean4

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

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