bUnion_ptsOfPeriod — Mathlib

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]

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