map — Mathlib

English

If x is periodic with period n for fa and g semiconjugates fa to fb, then g(x) is periodic for fb with the same period n.

Русский

Если x — периодическая точка fa с периодом n и g полусогласует fa с fb, то g(x) периодическая точка fb с периодом n.

LaTeX

$$$IsPeriodicPt fa n x \to Semiconj g fa fb \to IsPeriodicPt fb n (g x)$$$

Lean4

protected theorem map (hx : IsPeriodicPt fa n x) {g : α → β} (hg : Semiconj g fa fb) : IsPeriodicPt fb n (g x) :=
  IsFixedPt.map hx (hg.iterate_right n)

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