apply_mem_fixedPoints_iff_mem_of_mem_centralizer

English

If g and p commute (p lies in the centralizer of g), then p preserves the fixed points of g: for all x, p x is a fixed point of g iff x is a fixed point of g.

Русский

Если g и p commuting, то p сохраняет точки, фиксируемые g: для всех x верно, что p x фиксирована g тогда и только если x фиксирована g.

LaTeX

$$$p \\in \\mathrm{Centralizer}(\{g\\}) \\implies \\forall x:\\alpha,\\ p x \\in \\mathrm{Fix}(g) \\iff x \\in \\mathrm{Fix}(g).$$$

Lean4

theorem apply_mem_fixedPoints_iff_mem_of_mem_centralizer {g p : Perm α} (hp : p ∈ Subgroup.centralizer { g }) {x : α} :
    p x ∈ Function.fixedPoints g ↔ x ∈ Function.fixedPoints g :=
  by
  simp only [Subgroup.mem_centralizer_singleton_iff] at hp
  simp only [Function.mem_fixedPoints_iff]
  rw [← mul_apply, ← hp, mul_apply, EmbeddingLike.apply_eq_iff_eq]

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