English
If g and h commute, then h^j moves the moved-by set by g in the same way as the fixed set, i.e., h^j • (fixedBy α g)^c = (fixedBy α g)^c.
Русский
Если g и h коммутируют, то h^j перемещает множество, перемещаемое g, так же, как и фиксированное множество: h^j • (fixedBy α g)^c = (fixedBy α g)^c.
LaTeX
$$$ h^{j} \cdot (Set.instHasCompl.compl (MulAction.fixedBy α g)) = (Set.instHasCompl.compl (MulAction.fixedBy α g)) $$$
Lean4
/-- If `g` and `h` commute, then `g` moves `h • x` iff `g` moves `x`.
This is equivalent to say that the set `(fixedBy α g)ᶜ` is fixed by `h`.
-/
@[to_additive /-- If `g` and `h` commute, then `g` moves `h +ᵥ x` iff `g` moves `x`.
This is equivalent to say that the set `(fixedBy α g)ᶜ` is fixed by `h`. -/
]
theorem movedBy_mem_fixedBy_of_commute {g h : G} (comm : Commute g h) : (fixedBy α g)ᶜ ∈ fixedBy (Set α) h := by
rw [mem_fixedBy, Set.smul_set_compl, fixedBy_mem_fixedBy_of_commute comm]
