restrict_biUnion_finset — Mathlib

English

Let μ be a measure and ι a index set. If T is a countable index set and s_i are pairwise Disjoint, then μ.restrict (⋃ i ∈ T, s_i) = sum_{i∈T} μ.restrict (s_i).

Русский

Пусть μ — мера, ι — индексное множество. Если T счётно, а s_i попарно непересекаются, то ограничение по объединению равно сумме ограничений.

LaTeX

$$$\\mu\\restrict (\\bigcup_{i\\in T} s_i) = \\sum_{i\\in T} (\\mu\\restrict (s_i)).$$$

Lean4

theorem restrict_biUnion_finset {s : ι → Set α} {T : Finset ι} (hd : T.toSet.Pairwise (Disjoint on s))
    (hm : ∀ i, MeasurableSet (s i)) : μ.restrict (⋃ i ∈ T, s i) = sum fun (i : T) => μ.restrict (s i) :=
  restrict_biUnion (T := T.toSet) Finite.to_countable hd hm

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