prod_sum_left — Mathlib

English

For a countable index set, the sum inside a product distributes: (sum m) × μ equals sum of m_i × μ.

Русский

Для счётного множителя сумма внутри произведения дистрибуирует: (sum m) × μ = sum (m_i × μ).

LaTeX

$$ (Measure.sum m).prod μ = Measure.sum (fun i => (m i).prod μ)$$

Lean4

theorem prod_sum_left {ι : Type*} (m : ι → Measure α) (μ : Measure β) [SFinite μ] :
    (Measure.sum m).prod μ = Measure.sum (fun i ↦ (m i).prod μ) :=
  by
  ext s hs
  simp only [prod_apply hs, lintegral_sum_measure, hs, sum_apply]

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