Theorems · Theorem · Lie groups

MeasureTheory.eventually_nhds_one_measure_smul_sdiff_lt

∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : Group G] [IsTopologicalGroup G] [LocallyCompactSpace G] [MeasureTheory.IsFiniteMeasureOnCompacts μ]
  [μ.InnerRegularCompactLTTop] {k : Set G},
  IsCompact k → IsClosed k → ∀ {ε : ENNReal}, ε ≠ 0 → ∀ᶠ (g : G) in nhds 1, μ (g • k \ k) < ε

Continuity of the measure of translates of a compact set: Given a compact set k in a topological group, for g close enough to the origin, μ (g • k \ k) is arbitrarily small.

Defined in

Mathlib.MeasureTheory.Group.Measure

Cited by

3 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceBorelSpaceGroupIsTopologicalGroupLocallyCompactSpaceMeasureTheory.IsFiniteMeasureOnCompactsMeasureTheory.Measure.InnerRegularCompactLTTop