bijOn_periodicPts — Mathlib

English

The map f restricts to a bijection on the set of periodic points of f; i.e., f permutes the periodic points.

Русский

Отображение f ограничено на множество периодических точек и является биекцией на этом множестве; то есть f переставляет периодические точки.

LaTeX

$$$ \\operatorname{BijOn} f (\\operatorname{periodicPts} f) (\\operatorname{periodicPts} f) $$$

Lean4

theorem bijOn_periodicPts : BijOn f (periodicPts f) (periodicPts f) :=
  iUnion_pnat_ptsOfPeriod f ▸ bijOn_iUnion_of_directed (directed_ptsOfPeriod_pnat f) fun i => bijOn_ptsOfPeriod f i.pos

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