fundamentalFrontier_smul — Mathlib

English

For any g in a group H that commutes with G on α, the frontier transforms compatibly under the action: fundamentalFrontier(G, g·s) = g·fundamentalFrontier(G,s).

Русский

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

LaTeX

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

Lean4

@[to_additive (attr := simp) MeasureTheory.addFundamentalFrontier_vadd]
theorem fundamentalFrontier_smul [Group H] [MulAction H α] [SMulCommClass H G α] (g : H) :
    fundamentalFrontier G (g • s) = g • fundamentalFrontier G s := by
  simp_rw [fundamentalFrontier, smul_set_inter, smul_set_iUnion, smul_comm g (_ : G) (_ : Set α)]

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