mapsTo_periodicPts — Mathlib

English

If g is a semiconjugacy from fa to fb, then for every x, if x is periodic for fa, then g(x) is periodic for fb.

Русский

Если g является полупривязкой fa к fb, то для каждой x, если x периодично относительно fa, то g(x) периодично относительно fb.

LaTeX

$$$$ \\text{If } \\text{Semiconj}(g,fa,fb), \\; \\operatorname{MapsTo} \\big(g, \\operatorname{periodicPts}(fa), \\operatorname{periodicPts}(fb)\\big). $$$$

Lean4

theorem mapsTo_periodicPts {g : α → β} (h : Semiconj g fa fb) : MapsTo g (periodicPts fa) (periodicPts fb) :=
  fun _ ⟨n, hn, hx⟩ => ⟨n, hn, hx.map h⟩

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