iterate_right — Mathlib

English

If g is semiconjugate to f via ga and gb, then g is semiconjugate to the iterate ga^[n] and gb^[n].

Русский

Если g полусопряжен f через ga и gb, то g полусопряжен с ga^[n] и gb^[n].

LaTeX

$$$$\forall n, \; \mathrm{Semiconj}\ f\ ga^{[n]}\ gb^{[n]}. $$$$

Lean4

theorem iterate_right {f : α → β} {ga : α → α} {gb : β → β} (h : Semiconj f ga gb) (n : ℕ) : Semiconj f ga^[n] gb^[n] :=
  Nat.recOn n id_right fun _ ihn ↦ ihn.comp_right h

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