toNNReal_prod — Mathlib

English

For finite s and f: ι → ENNReal, the toNNReal of the finite product equals the product of the toNNReal values; i.e. (s.prod f).toNNReal = ∏_{i∈s} (f i).toNNReal.

Русский

Для конечного множества s и функции f: ι → ENNReal, toNNReal произведения равен произведению toNNReal отдельных элементов.

LaTeX

$$$$\\left( \\prod_{i\\in s} f(i) \\right)^{\\mathrm{toNNReal}} = \\prod_{i\\in s} f(i)^{\\mathrm{toNNReal}}$$$$

Lean4

@[simp]
theorem toNNReal_prod {ι : Type*} {s : Finset ι} {f : ι → ℝ≥0∞} : (∏ i ∈ s, f i).toNNReal = ∏ i ∈ s, (f i).toNNReal :=
  map_prod toNNRealHom _ _

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