# Almost everywhere disjoint sets #

We say that sets s and t are μ-a.e. disjoint (see MeasureTheory.AEDisjoint) if their intersection has measure zero. This assumption can be used instead of Disjoint in most theorems in measure theory.

def MeasureTheory.AEDisjoint {α : Type u_2} {m : } (μ : ) (s : Set α) (t : Set α) :

Two sets are said to be μ-a.e. disjoint if their intersection has measure zero.

Equations
• = (μ (s t) = 0)
Instances For
theorem MeasureTheory.exists_null_pairwise_disjoint_diff {ι : Type u_1} {α : Type u_2} {m : } {μ : } [] {s : ιSet α} (hd : ) :
∃ (t : ιSet α), (∀ (i : ι), MeasurableSet (t i)) (∀ (i : ι), μ (t i) = 0) Pairwise (Disjoint on fun (i : ι) => s i \ t i)

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 MeasureTheory.AEDisjoint.eq {α : Type u_2} {m : } {μ : } {s : Set α} {t : Set α} (h : ) :
μ (s t) = 0
theorem MeasureTheory.AEDisjoint.symm {α : Type u_2} {m : } {μ : } {s : Set α} {t : Set α} (h : ) :
theorem MeasureTheory.AEDisjoint.symmetric {α : Type u_2} {m : } {μ : } :
theorem MeasureTheory.AEDisjoint.comm {α : Type u_2} {m : } {μ : } {s : Set α} {t : Set α} :
theorem Disjoint.aedisjoint {α : Type u_2} {m : } {μ : } {s : Set α} {t : Set α} (h : Disjoint s t) :
theorem Pairwise.aedisjoint {ι : Type u_1} {α : Type u_2} {m : } {μ : } {f : ιSet α} (hf : Pairwise (Disjoint on f)) :
theorem Set.PairwiseDisjoint.aedisjoint {ι : Type u_1} {α : Type u_2} {m : } {μ : } {f : ιSet α} {s : Set ι} (hf : ) :
theorem MeasureTheory.AEDisjoint.mono_ae {α : Type u_2} {m : } {μ : } {s : Set α} {t : Set α} {u : Set α} {v : Set α} (h : ) (hu : ) (hv : ) :
theorem MeasureTheory.AEDisjoint.mono {α : Type u_2} {m : } {μ : } {s : Set α} {t : Set α} {u : Set α} {v : Set α} (h : ) (hu : u s) (hv : v t) :
theorem MeasureTheory.AEDisjoint.congr {α : Type u_2} {m : } {μ : } {s : Set α} {t : Set α} {u : Set α} {v : Set α} (h : ) (hu : ) (hv : ) :
@[simp]
theorem MeasureTheory.AEDisjoint.iUnion_left_iff {ι : Type u_1} {α : Type u_2} {m : } {μ : } {t : Set α} [] {s : ιSet α} :
MeasureTheory.AEDisjoint μ (⋃ (i : ι), s i) t ∀ (i : ι), MeasureTheory.AEDisjoint μ (s i) t
@[simp]
theorem MeasureTheory.AEDisjoint.iUnion_right_iff {ι : Type u_1} {α : Type u_2} {m : } {μ : } {s : Set α} [] {t : ιSet α} :
MeasureTheory.AEDisjoint μ s (⋃ (i : ι), t i) ∀ (i : ι), MeasureTheory.AEDisjoint μ s (t i)
@[simp]
theorem MeasureTheory.AEDisjoint.union_left_iff {α : Type u_2} {m : } {μ : } {s : Set α} {t : Set α} {u : Set α} :
@[simp]
theorem MeasureTheory.AEDisjoint.union_right_iff {α : Type u_2} {m : } {μ : } {s : Set α} {t : Set α} {u : Set α} :
theorem MeasureTheory.AEDisjoint.union_left {α : Type u_2} {m : } {μ : } {s : Set α} {t : Set α} {u : Set α} (hs : ) (ht : ) :
theorem MeasureTheory.AEDisjoint.union_right {α : Type u_2} {m : } {μ : } {s : Set α} {t : Set α} {u : Set α} (ht : ) (hu : ) :
theorem MeasureTheory.AEDisjoint.diff_ae_eq_left {α : Type u_2} {m : } {μ : } {s : Set α} {t : Set α} (h : ) :
theorem MeasureTheory.AEDisjoint.diff_ae_eq_right {α : Type u_2} {m : } {μ : } {s : Set α} {t : Set α} (h : ) :
theorem MeasureTheory.AEDisjoint.measure_diff_left {α : Type u_2} {m : } {μ : } {s : Set α} {t : Set α} (h : ) :
μ (s \ t) = μ s
theorem MeasureTheory.AEDisjoint.measure_diff_right {α : Type u_2} {m : } {μ : } {s : Set α} {t : Set α} (h : ) :
μ (t \ s) = μ t
theorem MeasureTheory.AEDisjoint.exists_disjoint_diff {α : Type u_2} {m : } {μ : } {s : Set α} {t : Set α} (h : ) :
∃ (u : Set α), μ u = 0 Disjoint (s \ u) t

If s and t are μ-a.e. disjoint, then s \ u and t are disjoint for some measurable null set u.

theorem MeasureTheory.AEDisjoint.of_null_right {α : Type u_2} {m : } {μ : } {s : Set α} {t : Set α} (h : μ t = 0) :
theorem MeasureTheory.AEDisjoint.of_null_left {α : Type u_2} {m : } {μ : } {s : Set α} {t : Set α} (h : μ s = 0) :
theorem MeasureTheory.aedisjoint_compl_left {α : Type u_2} {m : } {μ : } {s : Set α} :
theorem MeasureTheory.aedisjoint_compl_right {α : Type u_2} {m : } {μ : } {s : Set α} :