English
Under mild conditions, almost every set restricted to U lies in the codiscrete filter within U.
Русский
При умеренных условиях почти все множества, ограниченные до U, лежат в фильтре codiscreteWithin U.
LaTeX
$$$$\\ae(\\mu|_U) \\le \\operatorname{codiscreteWithin}(U).$$$$
Lean4
/-- Under reasonable assumptions, sets that are codiscrete within `U` are contained in the “almost
everywhere” filter of co-null sets. -/
theorem ae_restrict_le_codiscreteWithin {α : Type*} [MeasurableSpace α] [TopologicalSpace α] [SecondCountableTopology α]
{μ : Measure α} [NoAtoms μ] {U : Set α} (hU : MeasurableSet U) : ae (μ.restrict U) ≤ codiscreteWithin U :=
by
intro s hs
have := discreteTopology_of_codiscreteWithin hs
rw [mem_ae_iff, Measure.restrict_apply' hU]
apply Set.Countable.measure_zero (TopologicalSpace.separableSpace_iff_countable.1 inferInstance)
