English
If a countable family of sets is pairwise μ-almost everywhere disjoint, there exists a corresponding family of measurable null sets t_i such that s_i \ t_i are pairwise disjoint.
Русский
Если счётная семья множеств парно μ-пе-не пересечения, существует семейство измеримых нулевых множеств t_i так, что s_i \ t_i попарно непересекаются.
LaTeX
$$$\exists t : ι → Set α, (∀ i, MeasurableSet (t i)) ∧ (∀ i, μ(t i) = 0) ∧ Pairwise (Disjoint on (\lambda i, s i \ t i))$$$
Lean4
/-- If `s : ι → Set α` is a countable family of pairwise a.e. disjoint sets, then there exists a
family of measurable null sets `t i` such that `s i \ t i` are pairwise disjoint. -/
theorem exists_null_pairwise_disjoint_diff [Countable ι] {s : ι → Set α} (hd : Pairwise (AEDisjoint μ on s)) :
∃ t : ι → Set α, (∀ i, MeasurableSet (t i)) ∧ (∀ i, μ (t i) = 0) ∧ Pairwise (Disjoint on fun i => s i \ t i) :=
by
refine
⟨fun i => toMeasurable μ (s i ∩ ⋃ j ∈ ({ i }ᶜ : Set ι), s j), fun i => measurableSet_toMeasurable _ _, fun i => ?_,
?_⟩
· simp only [measure_toMeasurable, inter_iUnion]
exact (measure_biUnion_null_iff <| to_countable _).2 fun j hj => hd (Ne.symm hj)
· simp only [Pairwise, disjoint_left, onFun, mem_diff, not_and, and_imp, Classical.not_not]
intro i j hne x hi hU hj
replace hU : x ∉ s i ∩ iUnion fun j ↦ iUnion fun _ ↦ s j := fun h ↦ hU (subset_toMeasurable _ _ h)
simp only [mem_inter_iff, mem_iUnion, not_and, not_exists] at hU
exact (hU hi j hne.symm hj).elim
