Theorems · Theorem · measure theory

MeasureTheory.Measure.innerRegularWRT_preimage_one_hasCompactSupport_measure_ne_top_of_addGroup

∀ {G : Type u_2} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G]
  [inst_4 : MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant]
  [MeasureTheory.IsFiniteMeasureOnCompacts μ] [μ.InnerRegularCompactLTTop],
  μ.InnerRegularWRT (fun s => ∃ f, Continuous f ∧ HasCompactSupport f ∧ s = f ⁻¹' {1}) fun s =>
    MeasurableSet s ∧ μ s ≠ ⊤

Halmos' theorem: Haar measure is completion regular. More precisely, any finite measure set can be approximated from inside by a level set of a continuous function with compact support.

Defined in

Mathlib.MeasureTheory.Measure.EverywherePos

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddGroupTopologicalSpaceIsTopologicalAddGroupLocallyCompactSpaceMeasurableSpaceBorelSpaceMeasureTheory.Measure.IsAddLeftInvariantMeasureTheory.IsFiniteMeasureOnCompactsMeasureTheory.Measure.InnerRegularCompactLTTop