English
The Haar measure is regular.
Русский
Мера Хаара является регулярной.
LaTeX
$$(haarMeasure K0).Regular$$
Lean4
/-- **Steinhaus Theorem** for finite mass sets.
In any locally compact group `G` with an Haar measure `μ` that's inner regular on finite measure
sets, for any measurable set `E` of finite positive measure, the set `E / E` is a neighbourhood of
`1`. -/
@[to_additive /-- **Steinhaus Theorem** for finite mass sets.
In any locally compact group `G` with an Haar measure `μ` that's inner regular on finite measure
sets, for any measurable set `E` of finite positive measure, the set `E - E` is a neighbourhood of
`0`. -/
]
theorem div_mem_nhds_one_of_haar_pos_ne_top (μ : Measure G) [IsHaarMeasure μ] [LocallyCompactSpace G]
[μ.InnerRegularCompactLTTop] (E : Set G) (hE : MeasurableSet E) (hEpos : 0 < μ E) (hEfin : μ E ≠ ∞) :
E / E ∈ 𝓝 (1 : G) :=
steinhaus_mul_aux μ E hE <| hE.exists_lt_isCompact_of_ne_top hEfin hEpos
