Iterations of a function
In this file we prove simple properties of nat.iterate f n a.k.a. f^[n]:
iterate_zero,iterate_succ,iterate_succ',iterate_add,iterate_mul: formulas forf^[0],f^[n+1](two versions),f^[n+m], andf^[n*m];iterate_id:id^[n]=id;injective.iterate,surjective.iterate,bijective.iterate: iterates of an injective/surjective/bijective function belong to the same class;left_inverse.iterate,right_inverse.iterate,commute.iterate_left,comute.iterate_right,commute.iterate_iterate: some properties of pairs of functions survive under iterationsiterate_fixed,semiconj.iterate_*,semiconj₂.iterate: ifffixes a point (resp., semiconjugates unary/binary operarations), then so doesf^[n].
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 : ℕ) :
function.semiconj f ga^[n] 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 : ℕ) :
function.commute f g^[n]
theorem
function.commute.iterate_left
{α : Type u}
{f g : α → α}
(h : function.commute f g)
(n : ℕ) :
function.commute f^[n] g
theorem
function.commute.iterate_iterate
{α : Type u}
{f g : α → α}
(h : function.commute f g)
(m n : ℕ) :
function.commute f^[m] g^[n]
theorem
function.commute.iterate_eq_of_map_eq
{α : Type u}
{f g : α → α}
(h : function.commute f g)
(n : ℕ)
{x : α} :
theorem
function.commute.iterate_iterate_self
{α : Type u}
(f : α → α)
(m n : ℕ) :
function.commute f^[m] f^[n]
theorem
function.semiconj₂.iterate
{α : Type u}
{f : α → α}
{op : α → α → α}
(hf : function.semiconj₂ f op op)
(n : ℕ) :
function.semiconj₂ f^[n] op op
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 : ℕ) :