English
There are multiple equivalent ways to express SMul invariance under a group action: preimage invariance, image invariance, map invariance, and measure-preserving properties; all are equivalent.
Русский
Существует множество эквивалентных формулировок инвариантности по отношению к действию группы: инвариантность по предобразу, по образу, по отображению и по сохранению меры; все они эквивалентны.
LaTeX
$$$SMulInvariantMeasure\\ G\\ α\\ μ \\iff \\forall c,s\\ (MeasurableSet\\ s\\rightarrow μ((c\\cdot\\cdot)^{-1}(s))=μ(s)) \\iff \\forall c,s\\ (MeasurableSet\\ s\\rightarrow μ(c\\cdot s)=μ(s)) \\iff \\forall c\\ (map(c\\cdot)\\mu = \\mu) \\iff \\forall c\\ (MeasurePreserving(c\\cdot)\\mu\\mu).$$$
Lean4
@[to_additive (attr := simp)]
theorem eventuallyConst_smul_set_ae (c : G) {s : Set α} :
EventuallyConst (c • s : Set α) (ae μ) ↔ EventuallyConst s (ae μ) := by
rw [← preimage_smul_inv, eventuallyConst_preimage, Filter.map_smul, smul_ae]
