isPeriodicPt — Mathlib

English

A fixed point of f is a periodic point of f with any prescribed period.

Русский

Фиксированная точка f является периодической точкой для любого заданного периода.

LaTeX

$$$ \text{IsFixedPt}(f,x) \Rightarrow \text{IsPeriodicPt}(f,n,x). $$$

Lean4

/-- A fixed point of `f` is a periodic point of `f` of any prescribed period. -/
theorem isPeriodicPt (hf : IsFixedPt f x) (n : ℕ) : IsPeriodicPt f n x :=
  hf.iterate n

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