Almost everywhere disjoint sets #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We say that sets s and t are μ-a.e. disjoint (see measure_theory.ae_disjoint) if their
intersection has measure zero. This assumption can be used instead of disjoint in most theorems in
measure theory.
def
measure_theory.ae_disjoint
{α : Type u_2}
{m : measurable_space α}
(μ : measure_theory.measure α)
(s t : set α) :
Prop
Two sets are said to be μ-a.e. disjoint if their intersection has measure zero.
Equations
- measure_theory.ae_disjoint μ s t = (⇑μ (s ∩ t) = 0)
theorem
measure_theory.exists_null_pairwise_disjoint_diff
{ι : Type u_1}
{α : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[countable ι]
{s : ι → set α}
(hd : pairwise (measure_theory.ae_disjoint μ on s)) :
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.
@[protected]
theorem
measure_theory.ae_disjoint.eq
{α : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(h : measure_theory.ae_disjoint μ s t) :
@[protected, symm]
theorem
measure_theory.ae_disjoint.symm
{α : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(h : measure_theory.ae_disjoint μ s t) :
@[protected]
theorem
measure_theory.ae_disjoint.symmetric
{α : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α} :
@[protected]
theorem
measure_theory.ae_disjoint.comm
{α : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α} :
measure_theory.ae_disjoint μ s t ↔ measure_theory.ae_disjoint μ t s
@[protected]
theorem
disjoint.ae_disjoint
{α : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(h : disjoint s t) :
@[protected]
theorem
pairwise.ae_disjoint
{ι : Type u_1}
{α : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : ι → set α}
(hf : pairwise (disjoint on f)) :
@[protected]
theorem
set.pairwise_disjoint.ae_disjoint
{ι : Type u_1}
{α : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : ι → set α}
{s : set ι}
(hf : s.pairwise_disjoint f) :
s.pairwise (measure_theory.ae_disjoint μ on f)
theorem
measure_theory.ae_disjoint.mono_ae
{α : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s t u v : set α}
(h : measure_theory.ae_disjoint μ s t)
(hu : u ≤ᵐ[μ] s)
(hv : v ≤ᵐ[μ] t) :
@[protected]
theorem
measure_theory.ae_disjoint.mono
{α : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s t u v : set α}
(h : measure_theory.ae_disjoint μ s t)
(hu : u ⊆ s)
(hv : v ⊆ t) :
@[protected]
theorem
measure_theory.ae_disjoint.congr
{α : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s t u v : set α}
(h : measure_theory.ae_disjoint μ s t)
(hu : u =ᵐ[μ] s)
(hv : v =ᵐ[μ] t) :
@[simp]
theorem
measure_theory.ae_disjoint.Union_left_iff
{ι : Type u_1}
{α : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{t : set α}
[countable ι]
{s : ι → set α} :
measure_theory.ae_disjoint μ (⋃ (i : ι), s i) t ↔ ∀ (i : ι), measure_theory.ae_disjoint μ (s i) t
@[simp]
theorem
measure_theory.ae_disjoint.Union_right_iff
{ι : Type u_1}
{α : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[countable ι]
{t : ι → set α} :
measure_theory.ae_disjoint μ s (⋃ (i : ι), t i) ↔ ∀ (i : ι), measure_theory.ae_disjoint μ s (t i)
@[simp]
theorem
measure_theory.ae_disjoint.union_left_iff
{α : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s t u : set α} :
measure_theory.ae_disjoint μ (s ∪ t) u ↔ measure_theory.ae_disjoint μ s u ∧ measure_theory.ae_disjoint μ t u
@[simp]
theorem
measure_theory.ae_disjoint.union_right_iff
{α : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s t u : set α} :
measure_theory.ae_disjoint μ s (t ∪ u) ↔ measure_theory.ae_disjoint μ s t ∧ measure_theory.ae_disjoint μ s u
theorem
measure_theory.ae_disjoint.union_left
{α : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s t u : set α}
(hs : measure_theory.ae_disjoint μ s u)
(ht : measure_theory.ae_disjoint μ t u) :
measure_theory.ae_disjoint μ (s ∪ t) u
theorem
measure_theory.ae_disjoint.union_right
{α : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s t u : set α}
(ht : measure_theory.ae_disjoint μ s t)
(hu : measure_theory.ae_disjoint μ s u) :
measure_theory.ae_disjoint μ s (t ∪ u)
theorem
measure_theory.ae_disjoint.diff_ae_eq_left
{α : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(h : measure_theory.ae_disjoint μ s t) :
theorem
measure_theory.ae_disjoint.diff_ae_eq_right
{α : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(h : measure_theory.ae_disjoint μ s t) :
theorem
measure_theory.ae_disjoint.measure_diff_left
{α : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(h : measure_theory.ae_disjoint μ s t) :
theorem
measure_theory.ae_disjoint.measure_diff_right
{α : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(h : measure_theory.ae_disjoint μ s t) :
theorem
measure_theory.ae_disjoint.exists_disjoint_diff
{α : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(h : measure_theory.ae_disjoint μ s t) :
If s and t are μ-a.e. disjoint, then s \ u and t are disjoint for some measurable null
set u.
theorem
measure_theory.ae_disjoint.of_null_right
{α : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(h : ⇑μ t = 0) :
theorem
measure_theory.ae_disjoint.of_null_left
{α : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(h : ⇑μ s = 0) :
theorem
measure_theory.ae_disjoint_compl_left
{α : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s : set α} :
theorem
measure_theory.ae_disjoint_compl_right
{α : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s : set α} :