measure_mul_right_null — Mathlib

English

For a measurable set s and a left-invariant measure μ, translating s by right multiplication by y preserves the property that the preimage under right-translation has zero measure iff s has zero μ-measure.

Русский

Сдвиг множества s вправо на y сохраняет нулевую меру при взятии предобраза по правому умножению тогда и только тогда, когда μ(s) = 0.

LaTeX

$$$\mu((\cdot \cdot y)^{-1} s) = 0 \;\iff\; \mu(s) = 0$$$

Lean4

@[to_additive]
theorem measure_mul_right_null (y : G) : μ ((fun x => x * y) ⁻¹' s) = 0 ↔ μ s = 0 :=
  calc
    μ ((fun x => x * y) ⁻¹' s) = 0 ↔ μ ((fun x => y⁻¹ * x) ⁻¹' s⁻¹)⁻¹ = 0 := by
      simp_rw [← inv_preimage, preimage_preimage, mul_inv_rev, inv_inv]
    _ ↔ μ s = 0 := by simp only [measure_inv_null μ, measure_preimage_mul]

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