English
If f: G → H is a left-invariant morphism of groups with measurable structure and surjective, then the pushforward of a left-invariant μ is left-invariant.
Русский
Если f: G → H — морфизм групп слева с измеримой структурой и сюръект, то образ слева инвариантной μ остаётся слева инвариантной.
LaTeX
$$$f: G \to H$, hf measurable, h_surj surjective, IsMulLeftInvariant(μ) ⇒ IsMulLeftInvariant(Measure.map f μ)$$$
Lean4
/-- We shorten this from `measure_preimage_mul_left`, since left invariant is the preferred option
for measures in this formalization. -/
@[to_additive (attr := simp) /--
We shorten this from `measure_preimage_add_left`, since left invariant is the preferred option
for measures in this formalization. -/
]
theorem measure_preimage_mul (μ : Measure G) [IsMulLeftInvariant μ] (g : G) (A : Set G) :
μ ((fun h => g * h) ⁻¹' A) = μ A :=
calc
μ ((fun h => g * h) ⁻¹' A) = map (fun h => g * h) μ A := ((MeasurableEquiv.mulLeft g).map_apply A).symm
_ = μ A := by rw [map_mul_left_eq_self μ g]
