pow_apply_eq_self_of_apply_eq_self

English

If f fixes x (f(x) = x), then every power of f fixes x as well: (f^n)(x) = x for all n ∈ N.

Русский

Если f фиксирует x (f(x)=x), то любой степени f фиксирует x: (f^n)(x)=x для всех n ∈ ℕ.

LaTeX

$$$\forall x:\alpha,\ f(x)=x \Rightarrow \forall n:\mathbb{N},\ (f^n)(x)=x$$$

Lean4

theorem pow_apply_eq_self_of_apply_eq_self {x : α} (hfx : f x = x) : ∀ n : ℕ, (f ^ n) x = x
  | 0 => rfl
  | n + 1 => by rw [pow_succ, mul_apply, hfx, pow_apply_eq_self_of_apply_eq_self hfx n]

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