instIsMulLeftInvariant — Mathlib

English

If μ is right-invariant, then μ.inv is left-invariant.

Русский

Если μ справа инвариантна, то μ.inv слева инвариантна.

LaTeX

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

Lean4

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

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