smul_of_comm — Mathlib

English

If s is a fundamental domain and g ∈ G, then g • s is null-measurable.

Русский

Если s — фундаментальная область, то любой перенос g • s по группe также нулево измерим.

LaTeX

$$$\\text{NullMeasurableSet}(g\\cdot s, μ)$$$

Lean4

@[to_additive]
theorem smul_of_comm {G' : Type*} [Group G'] [MulAction G' α] [MeasurableSpace G'] [MeasurableSMul G' α]
    [SMulInvariantMeasure G' α μ] [SMulCommClass G' G α] (h : IsFundamentalDomain G s μ) (g : G') :
    IsFundamentalDomain G (g • s) μ :=
  h.image_of_equiv (MulAction.toPerm g) (measurePreserving_smul _ _).quasiMeasurePreserving (Equiv.refl _) <|
    smul_comm g

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