Theorems combining measure theory and topology #
This file gathers theorems that combine measure theory and topology, and cannot easily be added to the existing files without introducing massive dependencies between the subjects.
theorem
ae_restrict_le_codiscreteWithin
{α : Type u_1}
[MeasurableSpace α]
[TopologicalSpace α]
[SecondCountableTopology α]
{μ : MeasureTheory.Measure α}
[MeasureTheory.NoAtoms μ]
{U : Set α}
(hU : MeasurableSet U)
:
Under reasonable assumptions, sets that are codiscrete within U are contained in the “almost
everywhere” filter of co-null sets.