map_mul_right_ae — Mathlib

English

For a left-invariant μ, the set of x for which p(t·x) holds almost everywhere is the same as the set for which p(x) holds.

Русский

Для слева инвариантной μ множество x, где p(t·x) верно почти всюду, совпадает с множеством x, где p(x) верно почти всюду.

LaTeX

$$$(∀^{*} x, p(t\cdot x)) \iff (∀^{*} x, p(x))$ under IsMulLeftInvariant μ.$$

Lean4

@[to_additive]
theorem map_mul_right_ae (μ : Measure G) [IsMulRightInvariant μ] (x : G) : Filter.map (fun h => h * x) (ae μ) = ae μ :=
  ((MeasurableEquiv.mulRight x).map_ae μ).trans <| congr_arg ae <| map_mul_right_eq_self μ x

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