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;LeftInverse.iterate
,RightInverse.iterate
,Commute.iterate_left
,Commute.iterate_right
,Commute.iterate_iterate
: some properties of pairs of functions survive under iterationsiterate_fixed
,Function.Semiconj.iterate_*
,Function.Semiconj₂.iterate
: iff
fixes a point (resp., semiconjugates unary/binary operations), then so doesf^[n]
.
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_iterate_self
{α : Type u}
(f : α → α)
(m n : ℕ)
:
Function.Commute f^[m] f^[n]
theorem
Function.LeftInverse.iterate
{α : Type u}
{f g : α → α}
(hg : LeftInverse g f)
(n : ℕ)
:
LeftInverse g^[n] f^[n]
theorem
Function.RightInverse.iterate
{α : Type u}
{f g : α → α}
(hg : RightInverse g f)
(n : ℕ)
:
RightInverse g^[n] f^[n]
theorem
Function.iterate_commute
{α : Type u}
(m n : ℕ)
:
Function.Commute (fun (f : α → α) => f^[m]) fun (f : α → α) => f^[n]