measure_preimage_smul_le — Mathlib

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) _

Похожие утверждения