English
The set of periodic points is the union over all positive periods of the sets of points with a fixed period; i.e., periodic points are exactly those with some positive period.
Русский
Множество периодических точек есть объединение по всем положительным периодам множеств точек с данным периодом; другими словами, периодические точки — это те, у которых есть положительный период.
LaTeX
$$$$ \\bigcup_{n>0} \\operatorname{ptsOfPeriod}(f,n) = \\operatorname{periodicPts}(f). $$$$
Lean4
theorem bUnion_ptsOfPeriod : ⋃ n > 0, ptsOfPeriod f n = periodicPts f :=
Set.ext fun x => by simp [mem_periodicPts]