periodic_iterate_iff — Mathlib

English

For a function f on α, the sequence a, f(a), f^2(a), … is n-periodic iff a is a periodic point of f with period n.

Русский

Для функции f на α последовательность a, f(a), f^2(a), … периодична с периодом n тогда и только тогда, когда a является периодической точкой f с периодом n.

LaTeX

$$$\text{Periodic}((f^{[·]}a),n) \iff \text{IsPeriodicPt}(f,n,a).$$$

Lean4

/-- The iterates `a`, `f a`, `f^[2] a` etc form a periodic sequence with period `n`
iff `a` is a periodic point for `f`. -/
theorem periodic_iterate_iff {f : α → α} {n : ℕ} {a : α} : Periodic (f^[·] a) n ↔ IsPeriodicPt f n a :=
  by
  refine ⟨fun h ↦ h.eq, fun h k ↦ ?_⟩
  simp only [Function.iterate_add_apply, h.eq]

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