English
For a periodic point x, a point y lies in the periodic orbit of x if and only if there exists an n with y = f^n x.
Русский
Для периодической точки x точка y принадлежит периодической орбите x тогда и только тогда, когда существует n, такое что y = f^n x.
LaTeX
$$$\\forall x,y,\\ x\\in \\operatorname{periodicPts}(f)\\Rightarrow y \\in \\operatorname{periodicOrbit}(f,x) \\\\\\\iff \\exists n, f^{n}(x) = y$$$
Lean4
@[simp]
theorem mem_periodicOrbit_iff (hx : x ∈ periodicPts f) : y ∈ periodicOrbit f x ↔ ∃ n, f^[n] x = y :=
by
simp only [periodicOrbit, Cycle.mem_coe_iff, List.mem_map, List.mem_range]
use fun ⟨a, _, ha'⟩ => ⟨a, ha'⟩
rintro ⟨n, rfl⟩
use n % minimalPeriod f x, mod_lt _ (minimalPeriod_pos_of_mem_periodicPts hx)
rw [iterate_mod_minimalPeriod_eq]
