Theorems · Theorem · real analysis

Function.periodic_iterate_iff

∀ {α : Type u_1} {f : α → α} {n : ℕ} {a : α}, Function.Periodic (fun x => f^[x] a) n ↔ Function.IsPeriodicPt f n a

The iterates a, f a, f^[2] a etc form a periodic sequence with period n iff a is a periodic point for f.

Defined in

Mathlib.Algebra.Ring.Periodic

Cited by

2 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext