mapsTo_ptsOfPeriod — Mathlib

English

If g semiconjugates fa to fb, then for any n, g maps the fa-periodic points of period n to fb-periodic points of period n.

Русский

Если g полусогласует fa с fb, то для любого n отображение g переводит fa-периодические точки периода n в fb-периодические точки периода n.

LaTeX

$$Theorem mapsTo_ptsOfPeriod (h : Semiconj g fa fb) (n : ℕ) : MapsTo g (ptsOfPeriod fa n) (ptsOfPeriod fb n)$$

Lean4

theorem mapsTo_ptsOfPeriod {g : α → β} (h : Semiconj g fa fb) (n : ℕ) :
    MapsTo g (ptsOfPeriod fa n) (ptsOfPeriod fb n) :=
  (h.iterate_right n).mapsTo_fixedPoints

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