nullMeasurableSet_smul — Mathlib

English

For a fundamental domain h and ν ≪ μ, the sum of ν restricted to translates of s equals ν: sum_g ν|_{g•s} = ν.

Русский

Для фундаментальной области h и ν ≪ μ сумма ν, ограниченная переносами s, равна ν.

LaTeX

$$$\\sum_{g\\in G} \\nu \\restriction (g \\cdot s) = ν$$$

Lean4

@[to_additive]
theorem nullMeasurableSet_smul (h : IsFundamentalDomain G s μ) (g : G) : NullMeasurableSet (g • s) μ :=
  h.nullMeasurableSet.smul g

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