Documentation

Mathlib.Logic.Function.Iterate

Iterations of a function #

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

def Nat.iterate {α : Sort u} (op : αα) :
αα

Iterate a function.

Equations
Instances For

    Iterate a function.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[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 : ) :
      id^[n] = id
      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 : α} (hx : f x = g x) :
      f^[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 : } (hn : 0 < n) :
      f^[n.pred] f = f^[n]
      theorem Function.comp_iterate_pred_of_pos {α : Type u} (f : αα) {n : } (hn : 0 < n) :
      f f^[n.pred] = f^[n]
      def Function.Iterate.rec {α : Type u} (p : αSort u_1) {f : αα} (h : (a : α) → p ap (f a)) {a : α} (ha : p a) (n : ) :
      p (f^[n] a)

      A recursor for the iterate of a function.

      Equations
      Instances For
        theorem Function.Iterate.rec_zero {α : Type u} (p : αSort u_1) {f : αα} (h : (a : α) → p ap (f a)) {a : α} (ha : p a) :
        theorem Function.LeftInverse.iterate {α : Type u} {f : αα} {g : αα} (hg : Function.LeftInverse g f) (n : ) :
        theorem Function.RightInverse.iterate {α : Type u} {f : αα} {g : αα} (hg : Function.RightInverse g f) (n : ) :
        theorem Function.iterate_comm {α : Type u} (f : αα) (m : ) (n : ) :
        theorem Function.iterate_commute {α : Type u} (m : ) (n : ) :
        Function.Commute (fun (f : αα) => f^[m]) fun (f : αα) => f^[n]
        theorem Function.iterate_add_eq_iterate {α : Type u} {f : αα} {m : } {n : } {a : α} (hf : Function.Injective f) :
        f^[m + n] a = f^[n] a f^[m] a = a
        theorem Function.iterate_cancel_of_add {α : Type u} {f : αα} {m : } {n : } {a : α} (hf : Function.Injective f) :
        f^[m + n] a = f^[n] af^[m] a = a

        Alias of the forward direction of Function.iterate_add_eq_iterate.

        theorem Function.iterate_cancel {α : Type u} {f : αα} {m : } {n : } {a : α} (hf : Function.Injective f) (ha : f^[m] a = f^[n] a) :
        f^[m - n] a = a
        theorem Function.involutive_iff_iter_2_eq_id {α : Sort u_1} {f : αα} :
        theorem List.foldl_const {α : Type u} {β : Type v} (f : αα) (a : α) (l : List β) :
        List.foldl (fun (b : α) (x : β) => f b) a l = f^[l.length] a
        theorem List.foldr_const {α : Type u} {β : Type v} (f : ββ) (b : β) (l : List α) :
        List.foldr (fun (x : α) => f) b l = f^[l.length] b