haar_singleton — Mathlib

English

For Haar measure μ on a group G with ContinuousMul and BorelSpace, μ({g}) = μ({1}) for all g ∈ G.

Русский

Для меры Хаара μ на группе G с непрерывным умножением и борелевой топологией выполняется μ({g}) = μ({1}) для любого g.

LaTeX

$$$\mu\{g\} = \mu\{1\} \quad(\forall g \in G)$$$

Lean4

@[to_additive (attr := simp)]
theorem haar_singleton [ContinuousMul G] [BorelSpace G] (g : G) : μ { g } = μ {(1 : G)} :=
  by
  convert measure_preimage_mul μ g⁻¹ _
  simp only [mul_one, preimage_mul_left_singleton, inv_inv]

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