bijOn_ptsOfPeriod — Mathlib

English

For a positive n, the map f restricts to a bijection on the set of n-periodic points: f: ptsOfPeriod f n → ptsOfPeriod f n is bijective.

Русский

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

LaTeX

$$BijOn f (ptsOfPeriod f n) (ptsOfPeriod f n)$$

Lean4

theorem bijOn_ptsOfPeriod (f : α → α) {n : ℕ} (hn : 0 < n) : BijOn f (ptsOfPeriod f n) (ptsOfPeriod f n) :=
  ⟨(Commute.refl f).mapsTo_ptsOfPeriod n, fun _ hx _ hy hxy => hx.eq_of_apply_eq_same hy hn hxy, fun x hx =>
    ⟨f^[n.pred] x, hx.apply_iterate _, by rw [← comp_apply (f := f), comp_iterate_pred_of_pos f hn, hx.eq]⟩⟩

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