Function.Semiconj.iterate_right
theorem Function.Semiconj.iterate_right :
∀ {α : Type u} {β : Type v} {f : α → β} {ga : α → α} {gb : β → β},
Function.Semiconj f ga gb → ∀ (n : ℕ), Function.Semiconj f ga^[n] gb^[n]
The theorem `Function.Semiconj.iterate_right` states that for any types `α` and `β`, given a function `f` from `α` to `β`, and functions `ga : α → α` and `gb : β → β`, if `f` semiconjugates `ga` to `gb`, that is, `f ∘ ga = gb ∘ f`, then `f` also semiconjugates the `n`-th iteration of `ga` to the `n`-th iteration of `gb` for any natural number `n`. In other words, if `f` transforms every output of `ga` to the corresponding output of `gb`, it will do the same for `n` sequential applications of `ga` and `gb`.
More concisely: If function `f` semiconjugates `ga` to `gb`, then `f` semiconjugates the `n`-th iteration of `ga` to the `n`-th iteration of `gb` for any natural number `n`.
|
Function.iterate_cancel_of_add
theorem Function.iterate_cancel_of_add :
∀ {α : Type u} {f : α → α} {m n : ℕ} {a : α}, Function.Injective f → f^[m + n] a = f^[n] a → f^[m] a = a
The theorem `Function.iterate_cancel_of_add` states that for all types `α`, functions `f : α → α`, natural numbers `m` and `n`, and elements of `a : α`, if `f` is an injective function (i.e., a function that doesn't map distinct elements of `α` to the same element of `α`), and the `m + n`th iteration of `f` applied to `a` equals the `n`th iteration of `f` applied to `a`, then the `m`th iteration of `f` applied to `a` equals `a` itself. In simple terms, if repeating the function `f` `m + n` times on `a` yields the same result as repeating it `n` times, and `f` is injective, then repeating `f` `m` times on `a` brings us back to `a`.
More concisely: If a function `f : α → α` is injective and `m + n` applications of `f` to an element `a : α` yield the same result as `n` applications of `f` to `a`, then `m` applications of `f` to `a` equals `a`.
|
Function.iterate_succ_apply
theorem Function.iterate_succ_apply : ∀ {α : Type u} (f : α → α) (n : ℕ) (x : α), f^[n.succ] x = f^[n] (f x)
This theorem states that for any function `f` from a type `α` to itself, for any natural number `n`, and for any element `x` of type `α`, the `(n+1)`-th iteration of the function `f` applied to `x` is equal to the `n`-th iteration of `f` applied to the result of `f` on `x`. In other words, applying `f` `n + 1` times on `x` is the same as applying `f` once on `x` and then applying `f` `n` times on the result.
More concisely: For any function `f` from a type `α` to itself and any natural number `n` and element `x` of `α`, `f^(n+1)(x) = f(f^n(x))`.
|
Function.iterate_succ'
theorem Function.iterate_succ' : ∀ {α : Type u} (f : α → α) (n : ℕ), f^[n.succ] = f ∘ f^[n]
This theorem states that for any function `f` mapping a type `α` to itself and any natural number `n`, the `(n+1)`-th iteration of the function `f` is equivalent to the function `f` composed with the `n`-th iteration of `f`. In mathematical terms, given a function $f: \alpha \to \alpha$ and a natural number $n$, we have $f^{(n+1)} = f \circ f^{(n)}$, where $f^{(n)}$ denotes the `n`-th iteration of the function `f`, and $\circ$ denotes function composition.
More concisely: For any function $f: \alpha \to \alpha$ and natural number $n$, the $(n+1)$-th iteration of $f$ equals the composition of $f$ with the $n$-th iteration of $f$: $f^{(n+1)} = f \circ f^{(n)}$.
|
Function.Semiconj₂.iterate
theorem Function.Semiconj₂.iterate :
∀ {α : Type u} {f : α → α} {op : α → α → α},
Function.Semiconj₂ f op op → ∀ (n : ℕ), Function.Semiconj₂ f^[n] op op
The theorem `Function.Semiconj₂.iterate` states that for any type `α`, any function `f` from `α` to `α`, and any binary operation `op` on `α`, if `f` semiconjugates `op` to `op` (meaning that for all `x` and `y` in `α`, applying `f` after `op` is the same as applying `op` after `f`), then for any natural number `n`, the `n`-th iterate of `f` (i.e., applying `f` `n` times in succession) also semiconjugates `op` to `op`. In other words, the property of semiconjugating a binary operation is preserved under iteration of the function.
More concisely: If a function semiconjugates a binary operation, then the iteration of the function also semiconjugates the binary operation.
|
Function.iterate_fixed
theorem Function.iterate_fixed : ∀ {α : Type u} {f : α → α} {x : α}, f x = x → ∀ (n : ℕ), f^[n] x = x
This theorem states that for any type `α`, any function `f` from `α` to `α`, and any element `x` of `α`, if `f` applied to `x` gives `x` itself (i.e., `f x = x`), then for any natural number `n`, the `n`-times iteration of `f` applied to `x` will also yield `x`. In other words, if `x` is a fixed point of `f`, it remains the same under any number of iterations of `f`.
More concisely: If `f` is a function from type `α` to itself such that `f x = x` implies `fn x = x` for any natural number `n`, then `x` is a fixed point of `f`.
|
Function.iterate_succ
theorem Function.iterate_succ : ∀ {α : Type u} (f : α → α) (n : ℕ), f^[n.succ] = f^[n] ∘ f
This theorem, `Function.iterate_succ`, states that for any given function `f` mapping from a type `α` to itself and any natural number `n`, applying the function `f` `Nat.succ n` times (which is equivalent to `n + 1` times) is the same as first applying the function `f` `n` times and then applying `f` once more. This is expressed in terms of function composition (`∘`), which means applying one function and then another. This is a general property of functions and natural numbers in Lean 4.
More concisely: For any function f from type α to itself and natural number n, applying function f n+1 times is equivalent to applying function f n times and then applying function f once more. (Function composition: f ^ (n + 1) = f ^ n ∘ f)
|
Function.iterate_succ_apply'
theorem Function.iterate_succ_apply' : ∀ {α : Type u} (f : α → α) (n : ℕ) (x : α), f^[n.succ] x = f (f^[n] x) := by
sorry
This theorem states that for any function `f` of type `α → α` (meaning it takes an input of type `α` and returns an output of type `α`), any natural number `n`, and any `x` of type `α`, the application of the function `f` iterated `(n+1)` times to `x` is equivalent to applying `f` to the result of applying `f` `n` times to `x`. In the notation `f^[Nat.succ n] x`, `f^[Nat.succ n]` represents the function `f` iterated `(n+1)` times, and `x` is the input to this iterated function.
More concisely: For any function `f` of type `α → α` and any natural number `n` and input `x` of type `α`, applying `f` `(n+1)` times to `x` is equivalent to applying `f` `n` times and then once more to the result. In mathematical notation, `f^[Nat.succ n] x = f^[Nat.n] x <<< f x`, where `<<<` denotes function composition.
|
Function.Commute.iterate_right
theorem Function.Commute.iterate_right :
∀ {α : Type u} {f g : α → α}, Function.Commute f g → ∀ (n : ℕ), Function.Commute f g^[n]
This theorem states that for any type `α` and any two functions `f` and `g` from `α` to `α` that commute, the function `f` also commutes with the `n`-th iteration of `g` for any natural number `n`. Here, "commutes" means that composing `f` with `g` (i.e., `f(g(x))`) is the same as composing `g` with `f` (i.e., `g(f(x))`) for all `x` in `α`. The `n`-th iteration of `g` is the function obtained by applying `g` `n` times.
More concisely: For any type `α`, if functions `f` and `g` from `α` to `α` commute, then `f` commutes with the `n`-th power of `g` for all natural numbers `n`. (That is, `f(g^n(x)) = g^n(f(x))` for all `x` in `α`.)
|
Function.iterate_zero
theorem Function.iterate_zero : ∀ {α : Type u} (f : α → α), f^[0] = id
This theorem states that for every function `f` from type `α` to `α`, the zeroth iteration of `f` is the identity function. In other words, applying `f` zero times to any input produces the input itself. This is akin to raising a number to the power of zero - the output is always 1, the multiplicative identity. Here, instead of multiplication, we're doing function composition, and the identity function is the "do nothing" operation.
More concisely: For every function `f` from type `α` to `α`, the identity function is the identity of function composition with `f`, i.e., `id ∘ f = f ∘ id = f`.
|
Function.iterate_add_apply
theorem Function.iterate_add_apply : ∀ {α : Type u} (f : α → α) (m n : ℕ) (x : α), f^[m + n] x = f^[m] (f^[n] x) := by
sorry
This theorem, `Function.iterate_add_apply`, states that for any function `f` mapping a type `α` to itself, and for any natural numbers `m` and `n`, and for any element `x` of type `α`, the function `f` iterated (`m + n`) times on `x` is equal to the function `f` iterated `m` times on the result of `f` iterated `n` times on `x`. This is essentially a property of function iteration, similar to the concept of exponents in arithmetic where `(m + n)`-th power is the `m`-th power of the `n`-th power.
More concisely: For any function `f: α → α` and natural numbers `m` and `n`, `f^(m + n)(x) = f^m(f^n(x))`.
|
Function.Injective.iterate
theorem Function.Injective.iterate :
∀ {α : Type u} {f : α → α}, Function.Injective f → ∀ (n : ℕ), Function.Injective f^[n]
The theorem states that for any type `α` and any function `f` from `α` to `α`, if `f` is injective (that is, it never maps different inputs to the same output) then for any natural number `n`, the `n`-th iteration of `f` (denoted by `f^[n]`) is also injective. In other words, repeatedly applying an injective function still results in an injective function, no matter how many times you apply it.
More concisely: If `f` is an injective function from type `α` to itself, then for any natural number `n`, the `n`-th power of `f` is also an injective function.
|
Function.iterate_add
theorem Function.iterate_add : ∀ {α : Type u} (f : α → α) (m n : ℕ), f^[m + n] = f^[m] ∘ f^[n]
This theorem, named `Function.iterate_add`, is a property of function iteration in mathematics. For any function `f` from a type `α` to itself and any two natural numbers `m` and `n`, iterating the function `f` `(m + n)` times is equal to first iterating the function `f` `m` times and then iterating the result `n` times. In other words, it states that the application of `f` `(m + n)` times is the same as applying `f` `m` times, and then applying `f` `n` times to the result.
More concisely: For any function `f` from a type `α` to itself and natural numbers `m` and `n`, `(iterate f (m + n)) = (iterate f m) (iterate f n)`.
|
Function.iterate_one
theorem Function.iterate_one : ∀ {α : Type u} (f : α → α), f^[1] = f
This theorem states that for any function `f` from a type `α` to itself, iterating `f` once (i.e., applying `f` once to its argument) is equivalent to `f` itself. Here, `f^[1]` denotes the result of applying the function `f` once.
More concisely: For any function `f` from type `α`, `f^[1]` equals `f`.
|
Function.iterate_id
theorem Function.iterate_id : ∀ {α : Type u} (n : ℕ), id^[n] = id
This theorem, named `Function.iterate_id`, states that for any type `α` and natural number `n`, iterating the identity function (`id`) `n` times is equal to the identity function itself. In other words, no matter how many times you apply the identity function, the result is always the identity function.
More concisely: For any type `α` and natural number `n`, the repeated application of the identity function `n` times equals the identity function itself. (function composition) `id^n = id`
|
Function.iterate_zero_apply
theorem Function.iterate_zero_apply : ∀ {α : Type u} (f : α → α) (x : α), f^[0] x = x
This theorem states that for any function `f` that maps a type `α` to itself and any value `x` of type `α`, applying the function `f` zero times to `x` (denoted as `f^[0] x`) yields `x` itself. In other words, it formalizes the intuitive idea that not applying a function at all leaves the input unchanged.
More concisely: For any function `f` from type `α` to itself, `f^[0] x = x` for all `x : α`.
|
Function.Commute.iterate_left
theorem Function.Commute.iterate_left :
∀ {α : Type u} {f g : α → α}, Function.Commute f g → ∀ (n : ℕ), Function.Commute f^[n] g
This theorem states that for any types `α`, any two functions `f` and `g` from `α` to `α`, and any natural number `n`, if `f` and `g` commute (meaning `f (g x) = g (f x)` for all `x` in `α`), then `f` iterated `n` times and `g` also commute. In mathematical terms, if $f(g(x))=g(f(x))$ for all $x \in \alpha$, then $(f^n(g(x)))=g((f^n)(x))$ for any natural number $n$.
More concisely: If functions `f` and `g` from type `α` to `α` commute (i.e., `f (g x) = g (f x)` for all `x` in `α`), then `(f^n (g x)) = g ((f^n) x)` for any natural number `n`.
|
Function.iterate_mul
theorem Function.iterate_mul : ∀ {α : Type u} (f : α → α) (m n : ℕ), f^[m * n] = f^[m]^[n]
This theorem, called `Function.iterate_mul`, states that for any function `f` mapping a type `α` to itself and for any natural numbers `m` and `n`, the `m * n`th iteration of `f` is equal to the `n`th iteration of the `m`th iteration of `f`. In LaTeX, this is expressed as `f^{m * n} = (f^m)^n`. This means that if we apply the function `f` `m * n` times to a value, it's the same as applying the function `f` `m` times and then applying this new function `n` times.
More concisely: For any function $f$ from type $\alpha$ to itself, and natural numbers $m$ and $n$, the $m$th iteration of $f$ composed with the $n$th iteration equals the $m$th iteration of the $n$th iteration of $f$: $(f^m)^n = f^{m\cdot n}$.
|