Theorems · Theorem · real analysis

Function.Periodic.isPeriodicPt

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

Alias of the forward direction of Function.periodic_iterate_iff. 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

0 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext