distribHaarChar_eq_div — Mathlib

English

If μ is a Haar measure and s is a measurable set with μ(s) ≠ 0 and μ(s) ≠ ∞, then Δ(g) = μ(g•s)/μ(s).

Русский

Если μ — мера Хаара и s измеримо, с μ(s) ≠ 0, μ(s) ≠ ∞, тогда Δ(g) = μ(g•s)/μ(s).

LaTeX

$$$\\Delta(g) = \\dfrac{\\mu(g\\cdot S)}{\\mu(S)}, \\quad \\text{при } \\mu(S) \\neq 0, \\mu(S) \\neq \\infty.$$$

Lean4

theorem distribHaarChar_eq_div (hs₀ : μ s ≠ 0) (hs : μ s ≠ ∞) (g : G) : distribHaarChar A g = μ (g • s) / μ s := by
  rw [← distribHaarChar_mul, ENNReal.mul_div_cancel_right] <;> simp [*]

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