mathlib documentation

logic.function.iterate

Iterations of a function

In this file we prove simple properties of nat.iterate f n a.k.a. f^[n]:

@[simp]
theorem function.iterate_zero {α : Type u} (f : α → α) :
f^[0] = id

theorem function.iterate_zero_apply {α : Type u} (f : α → α) (x : α) :
f^[0] x = x

@[simp]
theorem function.iterate_succ {α : Type u} (f : α → α) (n : ) :
f^[n.succ] = f^[n] f

theorem function.iterate_succ_apply {α : Type u} (f : α → α) (n : ) (x : α) :
f^[n.succ] x = f^[n] (f x)

@[simp]
theorem function.iterate_id {α : Type u} (n : ) :

theorem function.iterate_add {α : Type u} (f : α → α) (m n : ) :
f^[m + n] = f^[m] (f^[n])

theorem function.iterate_add_apply {α : Type u} (f : α → α) (m n : ) (x : α) :
f^[m + n] x = f^[m] (f^[n] x)

@[simp]
theorem function.iterate_one {α : Type u} (f : α → α) :
f^[1] = f

theorem function.iterate_mul {α : Type u} (f : α → α) (m n : ) :
f^[m * n] = (f^[m]^[n])

theorem function.iterate_fixed {α : Type u} {f : α → α} {x : α} (h : f x = x) (n : ) :
f^[n] x = x

theorem function.injective.iterate {α : Type u} {f : α → α} (Hinj : function.injective f) (n : ) :

theorem function.surjective.iterate {α : Type u} {f : α → α} (Hsurj : function.surjective f) (n : ) :

theorem function.bijective.iterate {α : Type u} {f : α → α} (Hbij : function.bijective f) (n : ) :

theorem function.semiconj.iterate_right {α : Type u} {β : Type v} {f : α → β} {ga : α → α} {gb : β → β} (h : function.semiconj f ga gb) (n : ) :

theorem function.semiconj.iterate_left {α : Type u} {f : α → α} {g : α → α} (H : ∀ (n : ), function.semiconj f (g n) (g (n + 1))) (n k : ) :
function.semiconj f^[n] (g k) (g (n + k))

theorem function.commute.iterate_right {α : Type u} {f g : α → α} (h : function.commute f g) (n : ) :

theorem function.commute.iterate_left {α : Type u} {f g : α → α} (h : function.commute f g) (n : ) :

theorem function.commute.iterate_iterate {α : Type u} {f g : α → α} (h : function.commute f g) (m n : ) :

theorem function.commute.iterate_eq_of_map_eq {α : Type u} {f g : α → α} (h : function.commute f g) (n : ) {x : α} :
f x = g xf^[n] x = g^[n] x

theorem function.commute.comp_iterate {α : Type u} {f g : α → α} (h : function.commute f g) (n : ) :
f g^[n] = f^[n] (g^[n])

theorem function.commute.iterate_self {α : Type u} (f : α → α) (n : ) :

theorem function.commute.self_iterate {α : Type u} (f : α → α) (n : ) :

theorem function.commute.iterate_iterate_self {α : Type u} (f : α → α) (m n : ) :

theorem function.semiconj₂.iterate {α : Type u} {f : α → α} {op : α → α → α} (hf : function.semiconj₂ f op op) (n : ) :

theorem function.iterate_succ' {α : Type u} (f : α → α) (n : ) :
f^[n.succ] = f (f^[n])

theorem function.iterate_succ_apply' {α : Type u} (f : α → α) (n : ) (x : α) :
f^[n.succ] x = f (f^[n] x)

theorem function.iterate_pred_comp_of_pos {α : Type u} (f : α → α) {n : } :
0 < nf^[n.pred] f = (f^[n])

theorem function.comp_iterate_pred_of_pos {α : Type u} (f : α → α) {n : } :
0 < nf (f^[n.pred]) = (f^[n])

theorem function.left_inverse.iterate {α : Type u} {f g : α → α} (hg : function.left_inverse g f) (n : ) :

theorem function.right_inverse.iterate {α : Type u} {f g : α → α} (hg : function.right_inverse g f) (n : ) :