IsPeriodicPt — Mathlib

English

A point x is a periodic point of f with period n if f^[n](x) = x.

Русский

Точка x периодична для f с периодом n, если f^[n](x) = x.

LaTeX

$$$ \text{IsPeriodicPt}(f,n,x) \iff f^{[n]}(x) = x. $$$

Lean4

/-- A point `x` is a periodic point of `f : α → α` of period `n` if `f^[n] x = x`.
Note that we do not require `0 < n` in this definition. Many theorems about periodic points
need this assumption. -/
def IsPeriodicPt (f : α → α) (n : ℕ) (x : α) :=
  IsFixedPt f^[n] x

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