div_mem_nhds_one_of_haar_pos — Mathlib

English

In a second countable group, the Haar measure is sigma-finite.

Русский

Во второй счётной группе мера Хаара сигма-конечна.

LaTeX

$$SigmaFinite (haarMeasure K0)$$

Lean4

/-- **Steinhaus Theorem**.

In any locally compact group `G` with an inner regular Haar measure `μ`,
for any measurable set `E` of positive measure, the set `E / E` is a neighbourhood of `1`. -/
@[to_additive /-- **Steinhaus Theorem**.

    In any locally compact group `G` with an inner regular Haar measure `μ`,
    for any measurable set `E` of positive measure, the set `E - E` is a neighbourhood of `0`. -/
    ]
theorem div_mem_nhds_one_of_haar_pos (μ : Measure G) [IsHaarMeasure μ] [LocallyCompactSpace G] [InnerRegular μ]
    (E : Set G) (hE : MeasurableSet E) (hEpos : 0 < μ E) : E / E ∈ 𝓝 (1 : G) :=
  steinhaus_mul_aux μ E hE <| hE.exists_lt_isCompact hEpos

Похожие утверждения