English
If x is periodic with period n for fa and g semiconjugates fa to fb, then g(x) is periodic for fb with the same period n.
Русский
Если x — периодическая точка fa с периодом n и g полусогласует fa с fb, то g(x) периодическая точка fb с периодом n.
LaTeX
$$$IsPeriodicPt fa n x \to Semiconj g fa fb \to IsPeriodicPt fb n (g x)$$$
Lean4
protected theorem map (hx : IsPeriodicPt fa n x) {g : α → β} (hg : Semiconj g fa fb) : IsPeriodicPt fb n (g x) :=
IsFixedPt.map hx (hg.iterate_right n)