ThmDex – An index of mathematical definitions, results, and conjectures.
Set of symbols
Alphabet
Deduction system
Theory
Zermelo-Fraenkel set theory
Set
Binary cartesian set product
Binary relation
Map
Countable map
Sequence
Number sequence
Real function sequence
Rational sequence
Integer sequence
Natural number sequence
Definition D4594
Fibonacci natural number sequence
Formulation 0
A D997: Natural number sequence $F : \mathbb{N} \to \mathbb{N}$ is the Fibonacci natural number sequence if and only if
(1) $F_0 = 0$
(2) $F_1 = 1$
(3) $\forall \, n \geq 2 : F_n = F_{n - 1} + F_{n - 2}$
Formulation 1
Let $F : \mathbb{N} \to \mathbb{N}$ be a D997: Natural number sequence such that
(i) $F_0 = 0$
(ii) $F_1 = 1$
Then $F$ is the Fibonacci natural number sequence if and only if \begin{equation} F_2 = F_1 + F_0, \quad F_3 = F_2 + F_1, \quad F_4 = F_3 + F_2, \quad \dots \end{equation}