set_support_zpow_subset — Mathlib

English

For any integer n, the fixed points of p^n are contained among the fixed points of p.

Русский

Для любого целого n фиксированные точки p^n содержатся среди фиксированных точек p.

LaTeX

$$$$ \{x \mid (p^n)(x) \neq x\} \subseteq \{x \mid p(x) \neq x\}. $$$$

Lean4

theorem set_support_zpow_subset (n : ℤ) : {x | (p ^ n) x ≠ x} ⊆ {x | p x ≠ x} :=
  by
  intro x
  simp only [Set.mem_setOf_eq, Ne]
  intro hx H
  simp [zpow_apply_eq_self_of_apply_eq_self H] at hx

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