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.
Two sets are said to be μ-a.e. disjoint if their intersection has measure zero.
Equations
- MeasureTheory.AEDisjoint μ s t = (μ (s ∩ t) = 0)
Instances For
theorem
MeasureTheory.exists_null_pairwise_disjoint_sdiff
{ι : Type u_1}
{α : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[Countable ι]
{s : ι → Set α}
(hd : Pairwise (Function.onFun (AEDisjoint μ) s))
:
∃ (t : ι → Set α),
(∀ (i : ι), MeasurableSet (t i)) ∧ (∀ (i : ι), μ (t i) = 0) ∧ Pairwise (Function.onFun Disjoint 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.
@[deprecated MeasureTheory.exists_null_pairwise_disjoint_sdiff (since := "2026-06-03")]
theorem
MeasureTheory.exists_null_pairwise_disjoint_diff
{ι : Type u_1}
{α : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[Countable ι]
{s : ι → Set α}
(hd : Pairwise (Function.onFun (AEDisjoint μ) s))
:
∃ (t : ι → Set α),
(∀ (i : ι), MeasurableSet (t i)) ∧ (∀ (i : ι), μ (t i) = 0) ∧ Pairwise (Function.onFun Disjoint fun (i : ι) => s i \ t i)
Alias of MeasureTheory.exists_null_pairwise_disjoint_sdiff.
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 : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
(h : AEDisjoint μ s t)
:
theorem
MeasureTheory.AEDisjoint.symm
{α : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
(h : AEDisjoint μ s t)
:
AEDisjoint μ t s
instance
MeasureTheory.AEDisjoint.stdSymm
{α : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
:
Std.Symm (AEDisjoint μ)
@[deprecated MeasureTheory.AEDisjoint.stdSymm (since := "2026-06-10")]
theorem
MeasureTheory.AEDisjoint.symmetric
{α : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
:
Std.Symm (AEDisjoint μ)
Alias of MeasureTheory.AEDisjoint.stdSymm.
theorem
MeasureTheory.AEDisjoint.comm
{α : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
:
theorem
Disjoint.aedisjoint
{α : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s t : Set α}
(h : Disjoint s t)
:
MeasureTheory.AEDisjoint μ s t
theorem
Pairwise.aedisjoint
{ι : Type u_1}
{α : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : ι → Set α}
(hf : Pairwise (Function.onFun Disjoint f))
:
theorem
Set.PairwiseDisjoint.aedisjoint
{ι : Type u_1}
{α : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : ι → Set α}
{s : Set ι}
(hf : s.PairwiseDisjoint f)
:
s.Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) f)
theorem
MeasureTheory.AEDisjoint.mono_ae
{α : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{s t u v : Set α}
(h : AEDisjoint μ s t)
(hu : u ≤ᵐ[μ] s)
(hv : v ≤ᵐ[μ] t)
:
AEDisjoint μ u v
theorem
MeasureTheory.AEDisjoint.mono
{α : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{s t u v : Set α}
(h : AEDisjoint μ s t)
(hu : u ⊆ s)
(hv : v ⊆ t)
:
AEDisjoint μ u v
theorem
MeasureTheory.AEDisjoint.congr
{α : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{s t u v : Set α}
(h : AEDisjoint μ s t)
(hu : u =ᵐ[μ] s)
(hv : v =ᵐ[μ] t)
:
AEDisjoint μ u v
@[simp]
theorem
MeasureTheory.AEDisjoint.iUnion_left_iff
{α : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{t : Set α}
{ι : Sort u_3}
[Countable ι]
{s : ι → Set α}
:
@[simp]
theorem
MeasureTheory.AEDisjoint.iUnion_right_iff
{α : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
{ι : Sort u_3}
[Countable ι]
{t : ι → Set α}
:
@[simp]
theorem
MeasureTheory.AEDisjoint.union_left_iff
{α : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{s t u : Set α}
:
@[simp]
theorem
MeasureTheory.AEDisjoint.union_right_iff
{α : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{s t u : Set α}
:
theorem
MeasureTheory.AEDisjoint.union_left
{α : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{s t u : Set α}
(hs : AEDisjoint μ s u)
(ht : AEDisjoint μ t u)
:
AEDisjoint μ (s ∪ t) u
theorem
MeasureTheory.AEDisjoint.union_right
{α : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{s t u : Set α}
(ht : AEDisjoint μ s t)
(hu : AEDisjoint μ s u)
:
AEDisjoint μ s (t ∪ u)
theorem
MeasureTheory.AEDisjoint.sdiff_ae_eq_left
{α : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
(h : AEDisjoint μ s t)
:
@[deprecated MeasureTheory.AEDisjoint.sdiff_ae_eq_left (since := "2026-06-03")]
theorem
MeasureTheory.AEDisjoint.diff_ae_eq_left
{α : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
(h : AEDisjoint μ s t)
:
theorem
MeasureTheory.AEDisjoint.sdiff_ae_eq_right
{α : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
(h : AEDisjoint μ s t)
:
@[deprecated MeasureTheory.AEDisjoint.sdiff_ae_eq_right (since := "2026-06-03")]
theorem
MeasureTheory.AEDisjoint.diff_ae_eq_right
{α : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
(h : AEDisjoint μ s t)
:
theorem
MeasureTheory.AEDisjoint.measure_sdiff_left
{α : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
(h : AEDisjoint μ s t)
:
@[deprecated MeasureTheory.AEDisjoint.measure_sdiff_left (since := "2026-06-03")]
theorem
MeasureTheory.AEDisjoint.measure_diff_left
{α : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
(h : AEDisjoint μ s t)
:
theorem
MeasureTheory.AEDisjoint.measure_sdiff_right
{α : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
(h : AEDisjoint μ s t)
:
@[deprecated MeasureTheory.AEDisjoint.measure_sdiff_right (since := "2026-06-03")]
theorem
MeasureTheory.AEDisjoint.measure_diff_right
{α : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
(h : AEDisjoint μ s t)
:
theorem
MeasureTheory.AEDisjoint.exists_disjoint_diff
{α : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
(h : AEDisjoint μ s 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 : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
(h : μ t = 0)
:
AEDisjoint μ s t
theorem
MeasureTheory.AEDisjoint.of_null_left
{α : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
(h : μ s = 0)
:
AEDisjoint μ s t
theorem
MeasureTheory.aedisjoint_compl_left
{α : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
:
AEDisjoint μ sᶜ s
theorem
MeasureTheory.aedisjoint_compl_right
{α : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
:
AEDisjoint μ s sᶜ