English
Let s_i be a family and t a countable set. Then (∀ᵐ x ∂μ.restrict (⋃ i ∈ t, s_i), p x) iff ∀ i ∈ t, ∀ᵐ x ∂μ.restrict (s_i), p x.
Русский
Пусть s_i — семейство множеств, t — счётное множество индексов. Тогда условие почти всюду на biUnion эквивалентно для каждого i в t отдельно.
LaTeX
$$$\\bigl(\\forallᵐ x \\partial μ.restrict (\\bigcup_{i \\in t} s_i), p(x)\\bigr) \\iff \\forall i \\in t, \\forallᵐ x \\partial μ.restrict (s_i), p(x).$$$
Lean4
theorem ae_restrict_biUnion_eq (s : ι → Set α) {t : Set ι} (ht : t.Countable) :
ae (μ.restrict (⋃ i ∈ t, s i)) = ⨆ i ∈ t, ae (μ.restrict (s i)) :=
by
haveI := ht.to_subtype
rw [biUnion_eq_iUnion, ae_restrict_iUnion_eq, ← iSup_subtype'']