comp_eq_sum_of_countable — Mathlib

English

If α is countable and singletons are measurable, then κ ∘ₘ μ equals the sum ∑_ω μ({ω}) κ(ω).

Русский

Если α счётно и единичные множества измеримы, то κ ∘ₘ μ равняется сумме ∑_ω μ({ω}) κ(ω).

LaTeX

$$κ ∘ₘ μ = Measure.sum (λ ω, μ {ω} • κ ω)$$

Lean4

theorem comp_eq_sum_of_countable [Countable α] [MeasurableSingletonClass α] :
    κ ∘ₘ μ = Measure.sum (fun ω ↦ μ { ω } • κ ω) := by
  ext s hs
  rw [Measure.sum_apply _ hs, Measure.bind_apply hs (by fun_prop)]
  simp [lintegral_countable', mul_comm]

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