Inductive Definition of Sequence

 It has been suggested that this page or section be merged into Principle of Recursive Definition. (Discuss)

Theorem

Let $X$ be a set.

Let $h \in \N$.

Let $a_i \in X$ for all $i \in \set {1, 2, \ldots, h}$.

Let $S$ be the set of all finite sequences whose codomains are in $X$.

Let $G: S \to X$ be a mapping.

Then there is a unique sequence $f$ whose codomain is in $X$ such that:

$f_i = \begin{cases} a_i & : i \in \set {1, 2, \ldots, h} \\ \map G {f_1, f_2, \ldots, f_{i - 1} } & : i \ge h + 1 \end{cases}$

Also known as

Such a definition for a sequence is also known as a recursive definition.