English
The periodic orbit is a cyclic sequence of distinct points: it has no repetitions.
Русский
Периодическая орбита представляет собой циклическую последовательность различных точек: повторяющиеся элементы отсутствуют.
LaTeX
$$$\\text{Nodup}(\\operatorname{periodicOrbit}(f,x))$$$
Lean4
theorem nodup_periodicOrbit : (periodicOrbit f x).Nodup :=
by
rw [periodicOrbit, Cycle.nodup_coe_iff, List.nodup_map_iff_inj_on List.nodup_range]
intro m hm n hn hmn
rw [List.mem_range] at hm hn
rwa [iterate_eq_iterate_iff_of_lt_minimalPeriod hm hn] at hmn