multiset_prod_map_rpow — Mathlib

English

For any multiset s and function f : s → NNReal, and real r, the product of f’s values raised to r equals the rth power of the product of f’s values.

Русский

Для мультимножества s и функции f : s → NNReal, и вещественного r, произведение f(i)^r по i ∈ s равно (∏ f(i))^r.

LaTeX

$$(s.map (fun i => (f i) ^ r)).prod = (s.map f).prod ^ r$$

Lean4

/-- `rpow` version of `Multiset.prod_map_pow` for `ℝ≥0`. -/
theorem multiset_prod_map_rpow {ι} (s : Multiset ι) (f : ι → ℝ≥0) (r : ℝ) :
    (s.map (f · ^ r)).prod = (s.map f).prod ^ r :=
  s.prod_hom' (rpowMonoidHom r) _

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