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