prod_rpow_of_ne_top — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem prod_rpow_of_ne_top {ι} {s : Finset ι} {f : ι → ℝ≥0∞} (hf : ∀ i ∈ s, f i ≠ ∞) (r : ℝ) :
    ∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r := by
  classical
    induction s using Finset.induction with
  | empty => simp
  | insert i s hi ih =>
    have h2f : ∀ i ∈ s, f i ≠ ∞ := fun i hi ↦ hf i <| mem_insert_of_mem hi
    rw [prod_insert hi, prod_insert hi, ih h2f, ← mul_rpow_of_ne_top <| hf i <| mem_insert_self ..]
    apply prod_ne_top h2f

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