periodicOrbit_eq_nil_of_not_periodic_pt

English

If x is not periodic, then the periodic orbit of x is the empty cycle.

Русский

Если x не периодичен, то периодическая орбита x — пустой цикл.

LaTeX

$$$x \\notin \\operatorname{periodicPts}(f) \\Rightarrow \\operatorname{periodicOrbit}(f,x) = \\text{Cycle.nil}$$$

Lean4

theorem periodicOrbit_eq_nil_of_not_periodic_pt (h : x ∉ periodicPts f) : periodicOrbit f x = Cycle.nil :=
  periodicOrbit_eq_nil_iff_not_periodic_pt.2 h

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