Theorems · Theorem · measure theory

MeasureTheory.Measure.IsEverywherePos.IsGdelta_of_isMulLeftInvariant

∀ {G : Type u_2} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G]
  [inst_4 : MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [μ.IsMulLeftInvariant]
  [MeasureTheory.IsFiniteMeasureOnCompacts μ] [μ.InnerRegularCompactLTTop] {k : Set G},
  μ.IsEverywherePos k → IsCompact k → IsClosed k → IsGδ k

If a compact closed set is everywhere positive with respect to a left-invariant measure on a topological group, then it is a Gδ set. This is nontrivial, as there is no second-countability or metrizability assumption in the statement, so a general compact closed set has no reason to be a countable intersection of open sets.

Defined in

Mathlib.MeasureTheory.Measure.EverywherePos

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupTopologicalSpaceIsTopologicalGroupLocallyCompactSpaceMeasurableSpaceBorelSpaceMeasureTheory.Measure.IsMulLeftInvariantMeasureTheory.IsFiniteMeasureOnCompactsMeasureTheory.Measure.InnerRegularCompactLTTop