finset_prod_rpow — Mathlib

English

For any Finset s and f: s → Real with 0 ≤ f(i) for all i ∈ s, (∏ i∈s f(i)^r) = (∏ i∈s f(i))^r.

Русский

Для конечного множества s и функции f: s → Real с неотрицательностью значений, имеем (∏ i∈s f(i)^r) = (∏ i∈s f(i))^r.

LaTeX

$$∀ s f hl r, (∏ i ∈ s, (f i) ^ r) = (∏ i ∈ s, f i) ^ r$$

Lean4

/-- `rpow` version of `Finset.prod_pow`. -/
theorem _root_.Real.finset_prod_rpow {ι} (s : Finset ι) (f : ι → ℝ) (hs : ∀ i ∈ s, 0 ≤ f i) (r : ℝ) :
    (∏ i ∈ s, f i ^ r) = (∏ i ∈ s, f i) ^ r :=
  Real.multiset_prod_map_rpow s.val f hs r

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