English
If g and h commute, then h^j moves the complement of fixedBy α g by the same set, i.e., h^j • (fixedBy α g)^c = (fixedBy α g)^c for all j ∈ ℤ.
Русский
Если g и h commute, то h^j переносит множество (fixedBy α g)^c в себя: h^j • (fixedBy α g)^c = (fixedBy α g)^c для всех j ∈ ℤ.
LaTeX
$$$ h^{j} \cdot (fixedBy(α, g))^{c} = (fixedBy(α, g))^{c} $$$
Lean4
/-- If `g` and `h` commute, then `g` fixes `h • x` iff `g` fixes `x`.
This is equivalent to say that the set `fixedBy α g` is fixed by `h`.
-/
@[to_additive /-- If `g` and `h` commute, then `g` fixes `h +ᵥ x` iff `g` fixes `x`.
This is equivalent to say that the set `fixedBy α g` is fixed by `h`. -/
]
theorem fixedBy_mem_fixedBy_of_commute {g h : G} (comm : Commute g h) : (fixedBy α g) ∈ fixedBy (Set α) h :=
by
ext x
rw [Set.mem_smul_set_iff_inv_smul_mem, mem_fixedBy, ← mul_smul, comm.inv_right, mul_smul, smul_left_cancel_iff,
mem_fixedBy]
