finset_prod_rpow — Mathlib

English

For any finite index set s and f : s → NNReal with f(i) ≥ 0, (∏ i∈s f(i)^r) = (∏ i∈s f(i))^r for any real r.

Русский

Для конечного множества индексов s и функции f : s → NNReal с f(i) ≥ 0 выполняется (∏ i∈s f(i)^r) = (∏ i∈s f(i))^r.

LaTeX

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

Lean4

/-- `rpow` version of `Finset.prod_pow` for `ℝ≥0`. -/
theorem finset_prod_rpow {ι} (s : Finset ι) (f : ι → ℝ≥0) (r : ℝ) : (∏ i ∈ s, f i ^ r) = (∏ i ∈ s, f i) ^ r :=
  multiset_prod_map_rpow _ _
    _
      -- note: these don't really belong here, but they're much easier to prove in terms of the above

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