periodicPts — Mathlib

English

Let f be a map f: α → α. The periodic points of f are exactly those x for which there exists a positive integer n with f^n(x) = x.

Русский

Пусть f: α → α. Периодические точки f — это именно такие x, для которых существует положительное число n такое, что f^n(x) = x.

LaTeX

$$$$ \\operatorname{periodicPts}(f) = \\{ x \\in \\alpha \\mid \\exists n \\in \\mathbb{N},\\ n > 0 \\wedge f^n(x)=x \\}. $$$$

Lean4

/-- The set of periodic points of a map `f : α → α`. -/
def periodicPts (f : α → α) : Set α :=
  {x : α | ∃ n > 0, IsPeriodicPt f n x}

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