ofReal_prod_of_nonneg — Mathlib

English

If s is a finite set and f(i) ≥ 0 for all i ∈ s, then ENNReal.ofReal of the product equals the product of ENNReal.ofReal values: ENNReal.ofReal(∏_{i∈s} f(i)) = ∏_{i∈s} ENNReal.ofReal(f(i)).

Русский

Если s конечное и f(i) ≥ 0 для всех i∈s, то ENNReal.ofReal произведения равен произведению ENNReal.ofReal значений.

LaTeX

$$$$\\mathrm{ENNReal}.ofReal \\left( \\prod_{i\\in s} f(i) \\right) = \\prod_{i\\in s} \\mathrm{ENNReal}.ofReal(f(i))$$$$

Lean4

theorem ofReal_prod_of_nonneg {α : Type*} {s : Finset α} {f : α → ℝ} (hf : ∀ i, i ∈ s → 0 ≤ f i) :
    ENNReal.ofReal (∏ i ∈ s, f i) = ∏ i ∈ s, ENNReal.ofReal (f i) :=
  by
  simp_rw [ENNReal.ofReal, ← coe_finset_prod, coe_inj]
  exact Real.toNNReal_prod_of_nonneg hf

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