toReal_prod — Mathlib

English

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

Русский

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

LaTeX

$$$$\\left( \\prod_{i\\in s} f(i) \\right).toReal = \\prod_{i\\in s} f(i).toReal$$$$

Lean4

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

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