restrict_iUnion — Mathlib

English

Let s_i be a family of sets indexed by i ∈ ι and T a countable subset of ι. Then μ.restrict (⋃ i ∈ T, s_i) = sum_{i∈T} μ.restrict (s_i).

Русский

Пусть s_i — семействo множеств индексированных i ∈ ι, T — счётная подмножество индексов. Тогда ограничение объединения равно сумме ограничений по каждому s_i.

LaTeX

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

Lean4

theorem restrict_iUnion [Countable ι] {s : ι → Set α} (hd : Pairwise (Disjoint on s)) (hm : ∀ i, MeasurableSet (s i)) :
    μ.restrict (⋃ i, s i) = sum fun i => μ.restrict (s i) :=
  restrict_iUnion_ae hd.aedisjoint fun i => (hm i).nullMeasurableSet

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