toSMulInvariantMeasure_op — Mathlib

English

If μ is left-invariant under G, then μ viewed on the opposite group Gᵐᵒᵖ with the right action is SMulInvariantMeasure as well: SMulInvariantMeasure Gᵐᵒᵖ G μ.

Русский

Если μ слева инвариантна относительно G, то для противоположного пространства Gᵐᵒᵖ с правым действием μ сохраняет SMulInvariantMeasure: SMulInvariantMeasure Gᵐᵒᵖ G μ.

LaTeX

$$$\\text{SMulInvariantMeasure}(G^{\\text{op}}, G, μ)$$$

Lean4

@[to_additive]
instance toSMulInvariantMeasure_op [Mul G] [μ.IsMulRightInvariant] : SMulInvariantMeasure Gᵐᵒᵖ G μ :=
  ⟨fun _x _s hs => measure_preimage_of_map_eq_self (map_mul_right_eq_self _) hs.nullMeasurableSet⟩

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