smulInvariantMeasure — Mathlib

English

If a measure μ is left-invariant under multiplication by G, then the induced SMulInvariantMeasure structure on G acting on itself holds: SMulInvariantMeasure G G μ.

Русский

Если мера μ слева инвариантна относительно умножения на G, то образующая структура SMulInvariantMeasure для действия G на самой G выполняется: SMulInvariantMeasure G G μ.

LaTeX

$$$\\text{SMulInvariantMeasure}(G,G,\\mu)$ with the left-invariance condition$$

Lean4

@[to_additive]
instance smulInvariantMeasure [Mul G] [IsMulLeftInvariant μ] : SMulInvariantMeasure G G μ :=
  ⟨fun _x _s hs => measure_preimage_of_map_eq_self (map_mul_left_eq_self _) hs.nullMeasurableSet⟩

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