list_prod_map_rpow' — Mathlib

English

For any index type ι, a list l: List ι, f: ι → NNReal and r ∈ ℝ, (List.map (f ·^ r) l).prod = (List.map f l).prod^r.

Русский

Для типа индексов ι и списка l: List ι, функции f: ι → NNReal и вещественного r имеем: (l.map (f ·^ r)).prod = (l.map f).prod^r.

LaTeX

$$∀ {ι} (l : List ι) (f : ι → NNReal) (r : Real), (List.map (fun i => (f i) ^ r) l).prod = (List.map f l).prod ^ r$$

Lean4

theorem list_prod_map_rpow' {ι} (l : List ι) (f : ι → ℝ≥0) (r : ℝ) : (l.map (f · ^ r)).prod = (l.map f).prod ^ r := by
  rw [← list_prod_map_rpow, List.map_map]; rfl

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