Measures having value zero on singletons

TODO

Add a NoAtoms class defined as ∀ s, MeasurableSet s → 0 < μ s → ∃ t ⊆ s, MeasurableSet t ∧ 0 < μ t ∧ μ t < μ s. This implies NullSingletonClass but the converse is not true.

class MeasureTheory.NullSingletonClass {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) : Prop

Measure μ has value zero on singletons.

• measure_singleton (x : α) : μ {x} = 0

@[deprecated MeasureTheory.NullSingletonClass (since := "2026-06-09")]

def MeasureTheory.NoAtoms {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) : Prop

Alias of MeasureTheory.NullSingletonClass.

---

Measure μ has value zero on singletons.

Equations

• @MeasureTheory.NoAtoms = @MeasureTheory.NullSingletonClass

theorem Set.Subsingleton.measure_zero {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α} (hs : s.Subsingleton) (μ : MeasureTheory.Measure α) [MeasureTheory.NullSingletonClass μ] : μ s = 0

theorem MeasureTheory.Measure.restrict_singleton' {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] {a : α} : μ.restrict {a} = 0

instance MeasureTheory.Measure.restrict.instNullSingletonClass {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] (s : Set α) : NullSingletonClass (μ.restrict s)

theorem Set.Countable.measure_zero {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α} (h : s.Countable) (μ : MeasureTheory.Measure α) [MeasureTheory.NullSingletonClass μ] : μ s = 0

theorem Set.Countable.ae_notMem {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α} (h : s.Countable) (μ : MeasureTheory.Measure α) [MeasureTheory.NullSingletonClass μ] : ∀ᵐ (x : α) ∂μ, x ∉ s

theorem MeasureTheory.Measure.ae_ne {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) [NullSingletonClass μ] (a : α) : ∀ᵐ (x : α) ∂μ, x ≠ a

theorem Set.Countable.measure_restrict_compl {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α} (h : s.Countable) (μ : MeasureTheory.Measure α) [MeasureTheory.NullSingletonClass μ] : μ.restrict sᶜ = μ

@[simp]

theorem MeasureTheory.restrict_compl_singleton {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] (a : α) : μ.restrict {a}ᶜ = μ

theorem Set.Finite.measure_zero {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α} (h : s.Finite) (μ : MeasureTheory.Measure α) [MeasureTheory.NullSingletonClass μ] : μ s = 0

theorem Finset.measure_zero {α : Type u_1} {m0 : MeasurableSpace α} (s : Finset α) (μ : MeasureTheory.Measure α) [MeasureTheory.NullSingletonClass μ] : μ ↑s = 0

theorem MeasureTheory.insert_ae_eq_self {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] (a : α) (s : Set α) : insert a s =ᵐ[μ] s

theorem MeasureTheory.exists_accPt_of_nullSingletonClass {X : Type u_2} [TopologicalSpace X] [MeasurableSpace X] {μ : Measure X} [NullSingletonClass μ] {E : Set X} [TopologicalSpace.SeparableSpace ↑E] (hE : 0 < μ E) : ∃ (x : X), AccPt x (Filter.principal E)

@[deprecated MeasureTheory.exists_accPt_of_nullSingletonClass (since := "2026-06-09")]

theorem MeasureTheory.exists_accPt_of_noAtoms {X : Type u_2} [TopologicalSpace X] [MeasurableSpace X] {μ : Measure X} [NullSingletonClass μ] {E : Set X} [TopologicalSpace.SeparableSpace ↑E] (hE : 0 < μ E) : ∃ (x : X), AccPt x (Filter.principal E)

Alias of MeasureTheory.exists_accPt_of_nullSingletonClass.

theorem MeasureTheory.Iio_ae_eq_Iic {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] [PartialOrder α] {a : α} : Set.Iio a =ᵐ[μ] Set.Iic a

theorem MeasureTheory.Ioi_ae_eq_Ici {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] [PartialOrder α] {a : α} : Set.Ioi a =ᵐ[μ] Set.Ici a

theorem MeasureTheory.Ioo_ae_eq_Ioc {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] [PartialOrder α] {a b : α} : Set.Ioo a b =ᵐ[μ] Set.Ioc a b

theorem MeasureTheory.Ioc_ae_eq_Icc {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] [PartialOrder α] {a b : α} : Set.Ioc a b =ᵐ[μ] Set.Icc a b

theorem MeasureTheory.Ioo_ae_eq_Ico {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] [PartialOrder α] {a b : α} : Set.Ioo a b =ᵐ[μ] Set.Ico a b

theorem MeasureTheory.Ioo_ae_eq_Icc {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] [PartialOrder α] {a b : α} : Set.Ioo a b =ᵐ[μ] Set.Icc a b

theorem MeasureTheory.Ico_ae_eq_Icc {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] [PartialOrder α] {a b : α} : Set.Ico a b =ᵐ[μ] Set.Icc a b

theorem MeasureTheory.Ico_ae_eq_Ioc {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] [PartialOrder α] {a b : α} : Set.Ico a b =ᵐ[μ] Set.Ioc a b

theorem MeasureTheory.restrict_Iio_eq_restrict_Iic {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] [PartialOrder α] {a : α} : μ.restrict (Set.Iio a) = μ.restrict (Set.Iic a)

theorem MeasureTheory.restrict_Ioi_eq_restrict_Ici {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] [PartialOrder α] {a : α} : μ.restrict (Set.Ioi a) = μ.restrict (Set.Ici a)

theorem MeasureTheory.restrict_Ioo_eq_restrict_Ioc {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] [PartialOrder α] {a b : α} : μ.restrict (Set.Ioo a b) = μ.restrict (Set.Ioc a b)

theorem MeasureTheory.restrict_Ioc_eq_restrict_Icc {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] [PartialOrder α] {a b : α} : μ.restrict (Set.Ioc a b) = μ.restrict (Set.Icc a b)

theorem MeasureTheory.restrict_Ioo_eq_restrict_Ico {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] [PartialOrder α] {a b : α} : μ.restrict (Set.Ioo a b) = μ.restrict (Set.Ico a b)

theorem MeasureTheory.restrict_Ioo_eq_restrict_Icc {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] [PartialOrder α] {a b : α} : μ.restrict (Set.Ioo a b) = μ.restrict (Set.Icc a b)

theorem MeasureTheory.restrict_Ico_eq_restrict_Icc {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] [PartialOrder α] {a b : α} : μ.restrict (Set.Ico a b) = μ.restrict (Set.Icc a b)

theorem MeasureTheory.restrict_Ico_eq_restrict_Ioc {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] [PartialOrder α] {a b : α} : μ.restrict (Set.Ico a b) = μ.restrict (Set.Ioc a b)

theorem MeasureTheory.uIoc_ae_eq_interval {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] [LinearOrder α] {a b : α} : Set.uIoc a b =ᵐ[μ] Set.uIcc a b