instIsMulRightInvariant — Mathlib

English

If μ is left-invariant, then μ.inv is right-invariant; i.e., for all g and measurable A, μ.inv(A g) = μ.inv(A).

Русский

Если μ слева инвариантна, то μ.inv справа инвариантна; то есть для каждого g и измеримого A выполняется μ.inv(A g) = μ.inv(A).

LaTeX

$$$ \forall A, \; \mu^{\mathrm{inv}}(A g) = \mu^{\mathrm{inv}}(A) \quad \text{для всех } g \in G $$$

Lean4

@[to_additive]
instance instIsMulRightInvariant [IsMulLeftInvariant μ] : IsMulRightInvariant μ.inv :=
  by
  constructor
  intro g
  conv_rhs => rw [← map_mul_left_eq_self μ g⁻¹]
  simp_rw [Measure.inv, map_map (measurable_mul_const g) measurable_inv,
    map_map measurable_inv (measurable_const_mul g⁻¹), Function.comp_def, mul_inv_rev, inv_inv]

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