measurePreserving_div_right — Mathlib

English

If μ is left invariant on a group G, then the map x ↦ x/g preserves μ, i.e., μ((·/g)⁻¹A) = μ(A).

Русский

Если μ слева инвариантна на группе G, то карта x ↦ x/g сохраняет μ, то есть μ((·/g)⁻¹A) = μ(A).

LaTeX

$$$μ((\cdot / g)^{-1}A)=μ(A)$ for all A, given IsMulRightInvariant μ.$$

Lean4

@[to_additive]
theorem measurePreserving_div_right (μ : Measure G) [IsMulRightInvariant μ] (g : G) : MeasurePreserving (· / g) μ μ :=
  by simp_rw [div_eq_mul_inv, measurePreserving_mul_right μ g⁻¹]

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