fundamentalInterior_smul — Mathlib

English

For any g in group H commuting with G, the interior transforms under the action: fundamentalInterior(G, g·s) = g·fundamentalInterior(G,s).

Русский

При действии g из группы H, коммутирующей с G, внутренняя часть трансформируется аналогично: fundamentalInterior(G, g·s) = g·fundamentalInterior(G,s).

LaTeX

$$$\\mathrm{fundamentalInterior}(G, g \\cdot s) = g \\cdot \\mathrm{fundamentalInterior}(G,s)$$$

Lean4

@[to_additive (attr := simp) MeasureTheory.addFundamentalInterior_vadd]
theorem fundamentalInterior_smul [Group H] [MulAction H α] [SMulCommClass H G α] (g : H) :
    fundamentalInterior G (g • s) = g • fundamentalInterior G s := by
  simp_rw [fundamentalInterior, smul_set_sdiff, smul_set_iUnion, smul_comm g (_ : G) (_ : Set α)]

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