periodicOrbit_length — Mathlib

English

The length of the periodic orbit of x under f equals the minimal period of x under f.

Русский

Длина периодической орбиты x по f равна минимальному периоду x по f.

LaTeX

$$$\\lvert \\operatorname{periodicOrbit}(f,x) \\rvert = \\operatorname{minimalPeriod}(f,x)$$$

Lean4

@[simp]
theorem periodicOrbit_length : (periodicOrbit f x).length = minimalPeriod f x := by
  rw [periodicOrbit, Cycle.length_coe, List.length_map, List.length_range]

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