map_div_left_ae — Mathlib

English

For μ with left-invariance and inversion-invariance, the a.e. pushforward by t ↦ g / t leaves the a.e. class of μ unchanged: map (g / t) (ae μ) = (ae μ).

Русский

При μ, равномерно инвариантной слева и инверсии, отображение по a.e. слою t ↦ g / t не меняет эквивалентности по μ: map (g/t) (ae μ) = ae μ.

LaTeX

$$$ (\mathrm{Filter.map}\left( t \mapsto \tfrac{g}{t} \right) (\mathrm{ae}\,\mu)) = (\mathrm{ae}\,\mu) $$$

Lean4

@[to_additive]
theorem map_div_left_ae (μ : Measure G) [IsMulLeftInvariant μ] [IsInvInvariant μ] (x : G) :
    Filter.map (fun t => x / t) (ae μ) = ae μ :=
  ((MeasurableEquiv.divLeft x).map_ae μ).trans <| congr_arg ae <| map_div_left_eq_self μ x

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