self_mem_periodicOrbit — Mathlib

English

If x is a periodic point for f, then x itself lies in its periodic orbit: x ∈ periodicOrbit(f,x).

Русский

Если x — периодическая точка относительно f, то x принадлежит своей периодической орбите: x ∈ periodicOrbit(f,x).

LaTeX

$$$x \\in \\operatorname{periodicPts}(f) \\Rightarrow x \\in \\operatorname{periodicOrbit}(f,x)$$$

Lean4

theorem self_mem_periodicOrbit (hx : x ∈ periodicPts f) : x ∈ periodicOrbit f x := by simp [hx]

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