---
tag: 000MXHEY22
kind: statement
role: theorem
name: Sequential characterization of limits
aliases: [heine-definition-of-limit]
msc: [26A03]
uses: [0TXTSEMHR5, 0XKWSSY8P2]
sources:
  - url: https://en.wikipedia.org/wiki/Limit_of_a_function
    locator: In terms of sequences
---

## 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|0XKWSSY8P2]] 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.