User:Dfeuer/Principle of Recursive Definition/Peano Structure

Theorem

Let $(\N, 0, s)$ be a Peano structure, where $\N$ is a set.

Let $S$ be a non-empty set or class.

Let $f: S \to S$ be a mapping.

Let $c \in S$.

Then there is a unique mapping $g: \N \to S$ such that:

$g(0) = c$

$g(s(n)) = f(g(n))$ for all $n \in \N$

Proof

Let $\le$ be the usual ordering of $\N$.

Lemma

For each $n \in \N$ there is a unique mapping $g_n: {\downarrow} n \to S$ such that:

$$