periodicOrbit_eq_cycle_map — Mathlib

English

The periodic orbit can be expressed through a cycle map: periodicOrbit(f,x) equals the cycle obtained by mapping n to f^n x over the cycle of length minimalPeriod(f,x).

Русский

Периодическая орбита выражается через циклическое отображение: periodicOrbit(f,x) есть цикл, полученный отображением n → f^n x по циклу длины minimalPeriod(f,x).

LaTeX

$$$\\text{periodicOrbit}(f,x) = \\text{Cycle.map}(n \\mapsto f^{n}x)(\\text{Cycle.ofList}(\\text{List.range}(\\operatorname{minimalPeriod}(f,x))))$$$

Lean4

/-- The definition of a periodic orbit, in terms of `Cycle.map`. -/
theorem periodicOrbit_eq_cycle_map (f : α → α) (x : α) :
    periodicOrbit f x = (List.range (minimalPeriod f x) : Cycle ℕ).map fun n => f^[n] x :=
  rfl

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