English
The image of a left-invariant measure under a left action is left-invariant, provided the action preserves multiplication.
Русский
Образ слева инвариантной меры по левому действию сохраняет левую инвариантность, если действие сохраняет умножение.
LaTeX
$$$\\text{IsMulLeftInvariant}(μ) \\Rightarrow \\text{IsMulLeftInvariant}(map (a \\cdot \\·) μ)$ for any action by a on G.$$
Lean4
/-- The image of a left invariant measure under a left action is left invariant, assuming that
the action preserves multiplication. -/
@[to_additive /-- The image of a left invariant measure under a left additive action is left
invariant, assuming that the action preserves addition. -/
]
theorem isMulLeftInvariant_map_smul {α} [SMul α G] [SMulCommClass α G G] [MeasurableSpace α] [MeasurableSMul α G]
[IsMulLeftInvariant μ] (a : α) : IsMulLeftInvariant (map (a • · : G → G) μ) :=
(forall_measure_preimage_mul_iff _).1 fun x _ hs => (smulInvariantMeasure_map_smul μ a).measure_preimage_smul x hs
