haarMeasure_eq_iff — Mathlib

English

Haar is a canonical choice of a left-invariant measure on a locally compact group.

Русский

Хаар — канонический выбор лево-инвариантной меры на локально компактной группе.

LaTeX

$$haar[K0] = Haar measure on G$$

Lean4

/-- Let `μ` be a σ-finite left invariant measure on `G`. Then `μ` is equal to the Haar measure
defined by `K₀` iff `μ K₀ = 1`. -/
@[to_additive]
theorem haarMeasure_eq_iff (K₀ : PositiveCompacts G) (μ : Measure G) [SigmaFinite μ] [IsMulLeftInvariant μ] :
    haarMeasure K₀ = μ ↔ μ K₀ = 1 :=
  ⟨fun h => h.symm ▸ haarMeasure_self, fun h => by rw [haarMeasure_unique μ K₀, h, one_smul]⟩

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