ptsOfPeriod — Mathlib

English

The set of periodic points of a given (not necessarily minimal) period n is { x ∈ α | IsPeriodicPt f n x }.

Русский

Множество периодических точек для данного периода n равно { x ∈ α | IsPeriodicPt f n x }.

LaTeX

$$(ptsOfPeriod (f) n) = \{ x ∈ α \mid IsPeriodicPt f n x \}$$

Lean4

/-- The set of periodic points of a given (possibly non-minimal) period. -/
def ptsOfPeriod (f : α → α) (n : ℕ) : Set α :=
  {x : α | IsPeriodicPt f n x}

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