English
For countable ι with pairwise disjoint on s, μ restricted to the union of s i equals the sum of μ restricted to each s i evaluated at t, assuming each s i is measurable and t is measurable.
Русский
Для счётного ι с попарно непересекающимися на s множествами μ ограничено на объединение s_i равно сумме μ ограниченного на каждое s_i, при условии измеримости каждого s_i и t.
LaTeX
$$$[Countable\, ι] \ (Pairwise\, Disjoint\, on\, s) \land (∀ i, MeasurableSet (s i)) \land (MeasurableSet t) \Rightarrow \mu.restrict (\bigcup i, s i) t = \sum' i, \mu.restrict (s i) t$$$
Lean4
theorem restrict_iUnion_apply [Countable ι] {s : ι → Set α} (hd : Pairwise (Disjoint on s))
(hm : ∀ i, MeasurableSet (s i)) {t : Set α} (ht : MeasurableSet t) :
μ.restrict (⋃ i, s i) t = ∑' i, μ.restrict (s i) t :=
restrict_iUnion_apply_ae hd.aedisjoint (fun i => (hm i).nullMeasurableSet) ht
