mk_mem_periodicPts — Mathlib

English

If x has a period n > 0 under f (i.e., f^n(x) = x), then x is a periodic point: x ∈ periodicPts(f).

Русский

Если точка x имеет период n > 0 при f (то есть f^n(x) = x), то x является периодической точкой: x ∈ periodicPts(f).

LaTeX

$$$$ 0 < n \\quad \\text{and} \\quad f^n(x)=x \\quad\\Rightarrow\\quad x \\in \\operatorname{periodicPts}(f). $$$$

Lean4

theorem mk_mem_periodicPts (hn : 0 < n) (hx : IsPeriodicPt f n x) : x ∈ periodicPts f :=
  ⟨n, hn, hx⟩

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