English
A variant of the previous statement without an explicit hx; the chain condition is equivalent to the same pairwise relations along the orbit for all n.
Русский
Вариант предыдущего утверждения без явного условия о xo; условие цепи эквивалентно тем же попарным отношениям вдоль орбиты для всех n.
LaTeX
$$$(\\operatorname{periodicOrbit}(f,x)).Chain(r) \\iff \\forall n,\\ r(f^{n}x, f^{n+1}x)$$$
Lean4
theorem periodicOrbit_chain' (r : α → α → Prop) {f : α → α} {x : α} (hx : x ∈ periodicPts f) :
(periodicOrbit f x).Chain r ↔ ∀ n, r (f^[n] x) (f^[n + 1] x) :=
by
rw [periodicOrbit_chain r]
refine ⟨fun H n => ?_, fun H n _ => H n⟩
rw [iterate_succ_apply, ← iterate_mod_minimalPeriod_eq, ← iterate_mod_minimalPeriod_eq (n := n), ← iterate_succ_apply,
minimalPeriod_apply hx]
exact H _ (mod_lt _ (minimalPeriod_pos_of_mem_periodicPts hx))
