prod_sum — Mathlib

English

For a family of α-measures m i and a β-measure μ, the equality with sum distributes as above.

Русский

Для семейства мер по α и β выполняется распределение суммы над произведением.

LaTeX

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

Lean4

theorem prod_sum {ι ι' : Type*} [Countable ι'] (m : ι → Measure α) (m' : ι' → Measure β) [∀ n, SFinite (m' n)] :
    (Measure.sum m).prod (Measure.sum m') = Measure.sum (fun (p : ι × ι') ↦ (m p.1).prod (m' p.2)) := by
  simp_rw [prod_sum_left, prod_sum_right, sum_sum]

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