English
From a countable family of null measurable sets with pairwise disjointness, one can extract a subordinate family of measurable pairwise disjoint sets that are almost everywhere equal to the originals.
Русский
Из счётнойFamily нулевых измеримых паросочетанных множеств можно взять подпоследовательность измеримых попарно непересекающихся множеств, эквивалентных почти наверно исходным.
LaTeX
$$$\\exists t : ι → Set α, (∀ i, t(i) ⊆ s(i)) ∧ (∀ i, s(i) =^μ t(i)) ∧ (∀ i, MeasurableSet (t(i))) ∧ Pairwise (Disjoint on t)$$$
Lean4
/-- If `sᵢ` is a countable family of (null) measurable pairwise `μ`-a.e. disjoint sets, then there
exists a subordinate family `tᵢ ⊆ sᵢ` of measurable pairwise disjoint sets such that
`tᵢ =ᵐ[μ] sᵢ`. -/
theorem exists_subordinate_pairwise_disjoint [Countable ι] {s : ι → Set α} (h : ∀ i, NullMeasurableSet (s i) μ)
(hd : Pairwise (AEDisjoint μ on s)) :
∃ t : ι → Set α, (∀ i, t i ⊆ s i) ∧ (∀ i, s i =ᵐ[μ] t i) ∧ (∀ i, MeasurableSet (t i)) ∧ Pairwise (Disjoint on t) :=
by
choose t ht_sub htm ht_eq using fun i => exists_measurable_subset_ae_eq (h i)
rcases exists_null_pairwise_disjoint_diff hd with ⟨u, hum, hu₀, hud⟩
exact
⟨fun i => t i \ u i, fun i => diff_subset.trans (ht_sub _), fun i =>
(ht_eq _).symm.trans (diff_null_ae_eq_self (hu₀ i)).symm, fun i => (htm i).diff (hum i),
hud.mono fun i j h => h.mono (diff_subset_diff_left (ht_sub i)) (diff_subset_diff_left (ht_sub j))⟩
