periodicOrbit_eq_nil_iff_not_periodic_pt

English

The periodic orbit is empty if and only if x is not periodic under f.

Русский

Периодическая орбита пуста тогда и только тогда, когда x не периодичен по f.

LaTeX

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

Lean4

@[simp]
theorem periodicOrbit_eq_nil_iff_not_periodic_pt : periodicOrbit f x = Cycle.nil ↔ x ∉ periodicPts f :=
  by
  simp only [periodicOrbit.eq_1, Cycle.coe_eq_nil, List.map_eq_nil_iff, List.range_eq_nil]
  exact minimalPeriod_eq_zero_iff_notMem_periodicPts

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