English
If there is a semiconjugacy g from fa to fb, then g sends periodic points of fa to periodic points of fb; i.e., g maps periodicPts fa into periodicPts fb.
Русский
Если существует полууравнение g, переводящее fa в fb, то оно отображает периодические точки fa в периодические точки fb; то есть g отображает periodicPts fa в periodicPts fb.
LaTeX
$$$$ \\text{If } g \\circ fa = fb \\circ g, \\text{ then } g\\big(\\operatorname{periodicPts}(fa)\\big) \\subseteq \\operatorname{periodicPts}(fb). $$$$
Lean4
theorem isPeriodicPt_of_mem_periodicPts_of_isPeriodicPt_iterate (hx : x ∈ periodicPts f)
(hm : IsPeriodicPt f m (f^[n] x)) : IsPeriodicPt f m x :=
by
rcases hx with ⟨r, hr, hr'⟩
suffices n ≤ (n / r + 1) * r by
unfold IsPeriodicPt IsFixedPt
convert (hm.apply_iterate ((n / r + 1) * r - n)).eq <;>
rw [← iterate_add_apply, Nat.sub_add_cancel this, iterate_mul, (hr'.iterate _).eq]
rw [Nat.add_mul, one_mul]
exact (Nat.lt_div_mul_add hr).le
