measure_sUnion — Mathlib

English

Let S be a countable, pairwise disjoint family of measurable subsets of α. Then μ(⋃ S) = ∑' s ∈ S μ(s).

Русский

Пусть S — счетное множество попарно непересекающихся измеримых подмножеств пространства α. Тогда μ(⋃ S) = ∑_{s∈S} μ(s).

LaTeX

$$$$ \\mu\\left(\\bigcup_{s \\in S} s\\right) = \\sum_{s \\in S} \\mu(s). $$$$

Lean4

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

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