English
If a directed system of sets {s i} has countable index and t is measurable, then μ restricted to the union equals the supremum over i of μ restricted to s i evaluated at t.
Русский
Если система направленности множеств {s_i} счётна по индексу и t измеримо, то μ ограниченное на объединение равно супремуму по i от μ|_{s_i} на t.
LaTeX
$$$[Countable\, ι] \ (\text{hd : Directed (· ⊆ ·) } s) \land (ht : MeasurableSet t) \Rightarrow \mu.restrict (\bigcup_i s_i)\, t = \bigsup_i \mu.restrict (s_i)\, t$$$
Lean4
theorem restrict_iUnion_apply_ae [Countable ι] {s : ι → Set α} (hd : Pairwise (AEDisjoint μ on s))
(hm : ∀ i, NullMeasurableSet (s i) μ) {t : Set α} (ht : MeasurableSet t) :
μ.restrict (⋃ i, s i) t = ∑' i, μ.restrict (s i) t :=
by
simp only [restrict_apply, ht, inter_iUnion]
exact
measure_iUnion₀ (hd.mono fun i j h => h.mono inter_subset_right inter_subset_right) fun i =>
ht.nullMeasurableSet.inter (hm i)
