map_div_right_ae — Mathlib

English

If μ is right invariant, the a.e. image under division is μ-alike.

Русский

Если μ — правая инвариантность, то образ по делению почти наверняка равен μ.

LaTeX

$$$map (\cdot / x) (ae μ) = ae μ$ for IsMulRightInvariant μ.$$

Lean4

@[to_additive]
theorem map_div_right_ae (μ : Measure G) [IsMulRightInvariant μ] (x : G) : Filter.map (fun t => t / x) (ae μ) = ae μ :=
  ((MeasurableEquiv.divRight x).map_ae μ).trans <| congr_arg ae <| map_div_right_eq_self μ x

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