measure_mul_right_ne_zero — Mathlib

English

If s has positive measure under μ, then for every y, the μ-measure of the right-translated preimage is nonzero.

Русский

Если μ(s) ≠ 0, то для любого y мера множества предобраза по правому перемещению не равна нулю.

LaTeX

$$$\mu(s) \neq 0 \;\Rightarrow\; \mu((\cdot y)^{-1} s) \neq 0\quad\forall y$$$

Lean4

@[to_additive]
theorem measure_mul_right_ne_zero (h2s : μ s ≠ 0) (y : G) : μ ((fun x => x * y) ⁻¹' s) ≠ 0 :=
  (not_congr (measure_mul_right_null μ y)).mpr h2s

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