prod_rpow_of_nonneg — Mathlib

English

For a finite set s and f: s → ℝ≥0∞, and r ∈ ℝ with r ≥ 0, ∏ i∈s f(i)^r = (∏ i∈s f(i))^r.

Русский

Для конечного множества индексов s и f: s → ℝ≥0∞, при r ≥ 0 верно ∏ f(i)^r = (∏ f(i))^r.

LaTeX

$$$$\prod_{i \in s} f(i)^{r} = \left(\prod_{i \in s} f(i)\right)^{r} \quad \text{при } r \ge 0$$$$

Lean4

theorem prod_rpow_of_nonneg {ι} {s : Finset ι} {f : ι → ℝ≥0∞} {r : ℝ} (hr : 0 ≤ r) :
    ∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r := by
  classical
    induction s using Finset.induction with
  | empty => simp
  | insert _ _ hi ih => simp_rw [prod_insert hi, ih, ← mul_rpow_of_nonneg _ _ hr]

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