Theorems · Theorem · measure theory

ae_restrict_le_codiscreteWithin

∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [SecondCountableTopology α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.NullSingletonClass μ] {U : Set α},
  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.

Defined in

Mathlib.MeasureTheory.Topology

Cited by

4 results in Mathlib

Foundations

Depth 195 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceTopologicalSpaceSecondCountableTopologyMeasureTheory.NullSingletonClass