\begin{definition}[Definition:O Notation/Big-O Notation/Sequence]
Let $\sequence {a_n}$ and $\sequence {b_n}$ be sequences of real or complex numbers.
'''$a_n$ is big-O of $b_n$''' {{iff}}
:$\exists c \in \R_{\ge 0}: \exists n_0 \in \N: \forall n \in \N: \paren {n \ge n_0 \implies \size {a_n} \le c \cdot \size {b_n} }$
That is:
:$\size {a_n} \le c \cdot \size {b_n}$
for all sufficiently large $n$.
This is denoted:
:$a_n = \map \OO {b_n}$
\end{definition}