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.NullSingletonClass μ] {U : Set α} (hU : MeasurableSet U) : MeasureTheory.ae (μ.restrict U) ≤ Filter.codiscreteWithin U

Under reasonable assumptions, sets that are codiscrete within U are contained in the "almost everywhere" filter of co-null sets.