coe_finset_prod — Mathlib

English

For a finite set s and f: α → ℝ≥0, the ENNReal image of the NNReal product equals the product of ENNReal images: ↑(∏_{a∈s} f(a)) = ∏_{a∈s} (f(a)↑).

Русский

Для конечного множества s и функции f: α → ℝ≥0, ENNReal отображает произведение NNReal так же, как произведение ENNReal отображений: ↑(∏ f(a)) = ∏ ↑(f(a)).

LaTeX

$$$$\\uparrow\\left(\\prod_{a\\in s} f(a)\\right) = \\prod_{a\\in s} (f(a) : \\mathbb{R}_{\\ge 0}^{\\infty})$$$$

Lean4

@[simp, norm_cast]
theorem coe_finset_prod {s : Finset α} {f : α → ℝ≥0} : ↑(∏ a ∈ s, f a) = ∏ a ∈ s, (f a : ℝ≥0∞) :=
  map_prod ofNNRealHom f s

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