instSMulCommClassDomMulActNNReal

Mathlib.MeasureTheory.Group.MeasurableEquiv

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.instSMulCommClassDomMulActNNReal

English

For a measure μ on A and g ∈ Gᵈᵐᵃ, the action satisfies (g • μ)(s) = μ(DomMulAct.mk.symm g • s).

Русский

Для меры μ на A и элемента g ∈ Gᵈᵐᵃ выполняется (g • μ)(s) = μ(DomMulAct.mk.symm g • s).

LaTeX

$$$ (g \\cdot \\mu)(s) = \\mu(\\mathrm{DomMulAct.mk.un.symm}(g) \\cdot s) $$$

Lean4

instance : SMulCommClass Gᵈᵐᵃ ℝ≥0 (Measure A) :=
  .symm ..

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru