Définition d’une suite par récurrence

Définition formelle

Soient $X$ un ensemble, $f\to X$ une application et $a\in X$.
Alors il existe une unique suite $(u_n)_{n\in\mathbb N}$ à valeurs dans $X$ telle que :
$$u_0=a, \quad\forall n\in\mathbb N,\:u_{n+1}=f(u_n)$$

On dit que cette suite est définie par récurrence à partir de $a$ et de $f$.