Sequential characterization of limits

Statement

Let $D \subseteq \mathbb{R}$, let $f \colon D \to \mathbb{R}$, let $a$ be a limit point of $D$, and let $L$ be a real number. Then $\lim_{x \to a} f(x) = L$ if and only if the following holds. For each sequence $(x_n)$ in $D \setminus \{a\}$ with $x_n \to a$, $f(x_n) \to L$.

Remarks

This turns facts about limits of sequences into facts about limits of functions. Examples are the limit laws for sums, products, and quotients. It is also a tool to show that a limit does not exist. Find two sequences tending to $a$ whose images have different limits. Mathlib states a general form as tendsto_nhds_iff_seq_tendsto.

Explanations

L1 human

The function has limit $L$ at $a$ exactly when it sends every sequence approaching $a$ to a sequence approaching $L$. So limits of functions reduce to limits of sequences.