prod_coe_rpow — Mathlib

English

For a finite index set s, f: s → ℝ≥0, and r ∈ ℝ, the product of (f i)^{r} over i ∈ s equals the r-th power of the product of f i.

Русский

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

LaTeX

$$$$\prod_{i \in s} (f(i)^{r}) = \left(\prod_{i \in s} f(i)\right)^{r}$$$$

Lean4

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

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