English
For any c in G, the measure of the preimage of a set under the action by c is not larger than the measure of the set.
Русский
Для любого c в G мера предобраза множества под действием c не превосходит меру множества.
LaTeX
$$$\mu((c\cdot\cdot)^{-1'}s) \le \mu(s)$$$
Lean4
/-- See also `measure_preimage_smul_of_nullMeasurableSet` and `measure_preimage_smul`. -/
@[to_additive /-- See also `measure_preimage_smul_of_nullMeasurableSet` and `measure_preimage_smul`. -/
]
theorem measure_preimage_smul_le (c : G) (s : Set α) : μ ((c • ·) ⁻¹' s) ≤ μ s :=
(outerMeasure_le_iff (m := .map (c • ·) μ.1)).2 (fun _s hs ↦ (SMulInvariantMeasure.measure_preimage_smul _ hs).le) _