regular_haarMeasure — Mathlib

English

The Haar measure of the closure of K0 equals 1.

Русский

Мера Хаара замыкания K0 равна 1.

LaTeX

$$haarMeasure_K0(closure(K0)) = 1$$

Lean4

/-- The Haar measure is regular. -/
@[to_additive /-- The additive Haar measure is regular. -/
    ]
instance regular_haarMeasure {K₀ : PositiveCompacts G} : (haarMeasure K₀).Regular :=
  by
  haveI : LocallyCompactSpace G := K₀.locallyCompactSpace_of_group
  apply Regular.smul
  rw [← K₀.isCompact.measure_closure, Content.measure_apply _ isClosed_closure.measurableSet, ENNReal.inv_ne_top]
  exact (haarContent_outerMeasure_closure_pos K₀).ne'

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