periodicOrbit_def — Mathlib

English

The periodic orbit is given by the sequence of iterates x, f(x), f^2(x), ..., f^{p-1}(x) where p = minimalPeriod(f,x).

Русский

Периодическая орбита задаётся последовательностью x, f(x), f^2(x), ..., f^{p-1}(x), где p = minimalPeriod(f,x).

LaTeX

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

Lean4

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

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