English
For a countable index family, a property p holds almost everywhere with respect to μ.restrict (⋃ i, s_i) iff it holds almost everywhere with respect to μ.restrict (s_i) for all i.
Русский
Для счётной совокупности множеств свойство p имеет почти всюду относительно ограничений по объединению равно условию почти всюду относительно ограничений по каждому s_i.
LaTeX
$$$(\\forall i)(p\\text{ holds μ.restrict}(s_i)\,\\text{a.e.}) \\iff p\\text{ holds μ.restrict}(\\bigcup_i s_i)\\text{ a.e.}$$$
Lean4
@[simp]
theorem ae_restrict_iUnion_eq [Countable ι] (s : ι → Set α) : ae (μ.restrict (⋃ i, s i)) = ⨆ i, ae (μ.restrict (s i)) :=
le_antisymm ((ae_sum_eq fun i => μ.restrict (s i)) ▸ ae_mono restrict_iUnion_le) <|
iSup_le fun i => ae_mono <| restrict_mono (subset_iUnion s i) le_rfl
