of_disjoint_iUnion — Mathlib

English

Under measurability and disjointness, the measure of the union equals the sum (tsum) of the measures.

Русский

При измеримости и непересечности объединение множества равно сумме мер.

LaTeX

$$v (Set.iUnion fun i => f i) = ∑' i, v (f i)$$

Lean4

theorem of_disjoint_iUnion (hm : ∀ i, MeasurableSet (f i)) (hd : Pairwise (Disjoint on f)) :
    v (⋃ i, f i) = ∑' i, v (f i) :=
  (hasSum_of_disjoint_iUnion hm hd).tsum_eq.symm

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