Iteration of functions on natural numbers.

Copyright (c) The Iris-Lean Contributors.

theorem Nat.repeat_add {A : Type u_1} (n1 n2 : Nat) (f : A → A) (x : A) : «repeat» f (n1 + n2) x = «repeat» f n1 («repeat» f n2 x)

theorem Nat.repeat_apply_comm {α : Type u_1} (f : α → α) (k : Nat) (x : α) : «repeat» f k (f x) = f («repeat» f k x)

theorem Nat.repeat_fixed {α : Type u_1} (f : α → α) {x : α} (H : x = f x) (k : Nat) : x = «repeat» f k x

theorem Nat.repeat_rel {α : Type u_1} {R : α → α → Prop} (hR : Equivalence R) {f g : α → α} (hf : ∀ {x y : α}, R x y → R (f x) (f y)) (hfg : ∀ (z : α), R (f z) (g z)) (k : Nat) (z : α) : R («repeat» f k z) («repeat» g k z)

If f respects an equivalence R and is R-related to g pointwise, then iterating f and g gives R-related results.

theorem Nat.repeat_ind {α : Type u_1} (f : α → α) {P : α → Prop} (Hind : ∀ (x : α), P x → P (f x)) {x : α} (Hx : P x) (k : Nat) : P («repeat» f k x)