toNNReal_prod_of_nonneg — Mathlib

English

If f is nonnegative on a finite index set, Real.toNNReal of the product equals the product of Real.toNNReal.

Русский

Если f на конечном индексе неотрицателен, Real.toNNReal произведения равен произведению Real.toNNReal.

LaTeX

$$$$ Real.toNNReal(\\\\prod a \\\\in s, f a) = \\\\prod a \\\\in s, Real.toNNReal(f a). $$$$

Lean4

theorem _root_.Real.toNNReal_prod_of_nonneg (hf : ∀ a, a ∈ s → 0 ≤ f a) :
    Real.toNNReal (∏ a ∈ s, f a) = ∏ a ∈ s, Real.toNNReal (f a) :=
  by
  rw [← coe_inj, NNReal.coe_prod, Real.coe_toNNReal _ (Finset.prod_nonneg hf)]
  exact Finset.prod_congr rfl fun x hxs => by rw [Real.coe_toNNReal _ (hf x hxs)]

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