nodup_periodicOrbit — Mathlib

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

Похожие утверждения