iterate_left — Mathlib

English

If a family g satisfies a recurrence of semiconjugation with f, then f^{[n]} semiconjugates g(k) to g(n+k).

Русский

Если семейство g удовлетворяет рекуррентному полусопряжению, то f^{[n]} полусопрягивает g(k) к g(n+k).

LaTeX

$$$$\forall n,k, \; \mathrm{Semiconj} (\mathrm{Nat}.iterate f n) (g k) (g (n+k)). $$$$

Lean4

theorem iterate_left {g : ℕ → α → α} (H : ∀ n, Semiconj f (g n) (g <| n + 1)) (n k : ℕ) :
    Semiconj f^[n] (g k) (g <| n + k) := by
  induction n generalizing k with
  | zero =>
    rw [Nat.zero_add]
    exact id_left
  | succ n ihn =>
    rw [Nat.add_right_comm, Nat.add_assoc]
    exact (H k).trans (ihn (k + 1))

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