Measures having no atoms #
A measure μ has no atoms if the measure of each singleton is zero.
TODO #
Should NoAtoms be redefined as ∀ s, 0 < μ s → ∃ t ⊆ s, 0 < μ t ∧ μ t < μ s?
Measure μ has no atoms if the measure of each singleton is zero.
NB: Wikipedia assumes that for any measurable set s with positive μ-measure,
there exists a measurable t ⊆ s such that 0 < μ t < μ s. While this implies μ {x} = 0,
the converse is not true.
Instances
theorem
Set.Subsingleton.measure_zero
{α : Type u_1}
{m0 : MeasurableSpace α}
{s : Set α}
(hs : s.Subsingleton)
(μ : MeasureTheory.Measure α)
[MeasureTheory.NoAtoms μ]
:
theorem
MeasureTheory.Measure.restrict_singleton'
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NoAtoms μ]
{a : α}
:
instance
MeasureTheory.Measure.restrict.instNoAtoms
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NoAtoms μ]
(s : Set α)
:
theorem
Set.Countable.measure_zero
{α : Type u_1}
{m0 : MeasurableSpace α}
{s : Set α}
(h : s.Countable)
(μ : MeasureTheory.Measure α)
[MeasureTheory.NoAtoms μ]
:
theorem
Set.Countable.ae_not_mem
{α : Type u_1}
{m0 : MeasurableSpace α}
{s : Set α}
(h : s.Countable)
(μ : MeasureTheory.Measure α)
[MeasureTheory.NoAtoms μ]
:
theorem
Set.Countable.measure_restrict_compl
{α : Type u_1}
{m0 : MeasurableSpace α}
{s : Set α}
(h : s.Countable)
(μ : MeasureTheory.Measure α)
[MeasureTheory.NoAtoms μ]
:
theorem
Set.Finite.measure_zero
{α : Type u_1}
{m0 : MeasurableSpace α}
{s : Set α}
(h : s.Finite)
(μ : MeasureTheory.Measure α)
[MeasureTheory.NoAtoms μ]
:
theorem
Finset.measure_zero
{α : Type u_1}
{m0 : MeasurableSpace α}
(s : Finset α)
(μ : MeasureTheory.Measure α)
[MeasureTheory.NoAtoms μ]
:
theorem
MeasureTheory.Iio_ae_eq_Iic
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NoAtoms μ]
[PartialOrder α]
{a : α}
:
theorem
MeasureTheory.Ioi_ae_eq_Ici
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NoAtoms μ]
[PartialOrder α]
{a : α}
:
theorem
MeasureTheory.Ioo_ae_eq_Ioc
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NoAtoms μ]
[PartialOrder α]
{a b : α}
:
theorem
MeasureTheory.Ioc_ae_eq_Icc
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NoAtoms μ]
[PartialOrder α]
{a b : α}
:
theorem
MeasureTheory.Ioo_ae_eq_Ico
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NoAtoms μ]
[PartialOrder α]
{a b : α}
:
theorem
MeasureTheory.Ioo_ae_eq_Icc
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NoAtoms μ]
[PartialOrder α]
{a b : α}
:
theorem
MeasureTheory.Ico_ae_eq_Icc
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NoAtoms μ]
[PartialOrder α]
{a b : α}
:
theorem
MeasureTheory.Ico_ae_eq_Ioc
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NoAtoms μ]
[PartialOrder α]
{a b : α}
:
theorem
MeasureTheory.restrict_Iio_eq_restrict_Iic
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NoAtoms μ]
[PartialOrder α]
{a : α}
:
theorem
MeasureTheory.restrict_Ioi_eq_restrict_Ici
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NoAtoms μ]
[PartialOrder α]
{a : α}
:
theorem
MeasureTheory.restrict_Ioo_eq_restrict_Ioc
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NoAtoms μ]
[PartialOrder α]
{a b : α}
:
theorem
MeasureTheory.restrict_Ioc_eq_restrict_Icc
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NoAtoms μ]
[PartialOrder α]
{a b : α}
:
theorem
MeasureTheory.restrict_Ioo_eq_restrict_Ico
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NoAtoms μ]
[PartialOrder α]
{a b : α}
:
theorem
MeasureTheory.restrict_Ioo_eq_restrict_Icc
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NoAtoms μ]
[PartialOrder α]
{a b : α}
:
theorem
MeasureTheory.restrict_Ico_eq_restrict_Icc
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NoAtoms μ]
[PartialOrder α]
{a b : α}
:
theorem
MeasureTheory.restrict_Ico_eq_restrict_Ioc
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NoAtoms μ]
[PartialOrder α]
{a b : α}
:
theorem
MeasureTheory.uIoc_ae_eq_interval
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NoAtoms μ]
[LinearOrder α]
{a b : α}
: