measure_preimage_mul_right — Mathlib

English

If μ is left invariant, then the image under right multiplication is left invariant as well.

Русский

Если μ слева инвариантна, то изображение по правому умножению также инвариантно слева.

LaTeX

$$$IsMulLeftInvariant(μ) \Rightarrow IsMulLeftInvariant(map (x \cdot g) μ)$$$

Lean4

@[to_additive (attr := simp)]
theorem measure_preimage_mul_right (μ : Measure G) [IsMulRightInvariant μ] (g : G) (A : Set G) :
    μ ((fun h => h * g) ⁻¹' A) = μ A :=
  calc
    μ ((fun h => h * g) ⁻¹' A) = map (fun h => h * g) μ A := ((MeasurableEquiv.mulRight g).map_apply A).symm
    _ = μ A := by rw [map_mul_right_eq_self μ g]

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