measure_sUnion₀ — Mathlib

English

For a countable family of sets S, pairwise AEDisjoint, and each S element null-measurable, μ(⋃₀ S) equals the sum over S of μ.

Русский

Для счетного множества множеств S, попарно AEDisjoint, и каждого элемента S нулемеряемо, μ(union S) равно сумме μ.

LaTeX

$$$$\\forall S:\\mathrm Set (\\mathrm Set α),\\; S.Countable \\rightarrow S.Pairwise (\\mathrm AEDisjoint\\, \\mu) \\rightarrow (\\forall s \\in S, \\mathrm NullMeasurableSet s \\mu) \\rightarrow \\mu(\\bigcup_{s\\in S} s) = \\sum' s:\\, S, \\mu(s).$$$$

Lean4

theorem measure_sUnion₀ {S : Set (Set α)} (hs : S.Countable) (hd : S.Pairwise (AEDisjoint μ))
    (h : ∀ s ∈ S, NullMeasurableSet s μ) : μ (⋃₀ S) = ∑' s : S, μ s := by
  rw [sUnion_eq_biUnion, measure_biUnion₀ hs hd h]

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