A function has no limit at $c$ as soon as two sequences in $A \setminus \{c\}$ tending to $c$ give different limits of the values

Let $A \subseteq \mathbb{R}$, let $f : A \to \mathbb{R}$ and let $c$ be a limit point of $A$ (Limit point, isolated point, adherent point, derived set, and dense subset of $\mathbb{R}$). Then $f$ has no limit at $c$ — that is, no $L \in \mathbb{R}$ satisfies $\lim_{x \to c} f(x) = L$ (The $\varepsilon$-$\delta$ limit $\lim_{x \to c} f(x) = L$ of $f : A \to \mathbb{R}$ at a limit point $c$ of $A$) — as soon as either of the following occurs.

1. There are sequences $(x_k)$ and $(y_k)$ with all terms in $A \setminus \{c\}$, both converging to $c$, and reals $P \ne Q$ with $f(x_k) \to P$ and $f(y_k) \to Q$ (Sequences of reals: bounded, eventually, frequently, tails, subsequences, Limits and Cauchy sequences of reals).
2. There is a sequence $(x_k)$ with all terms in $A \setminus \{c\}$, converging to $c$, for which $(f(x_k))$ does not converge.

Only the choice-free half of the Heine criterion is used. The proof runs the implication from condition 1 to condition 2 of Heine criterion: $\lim_{x \to c} f(x) = L$ iff $f(x_k) \to L$ for every sequence in $A \setminus \{c\}$ converging to $c$, which is a theorem of ZF; no sequence is constructed here, both being supplied by the hypothesis. So this corollary, the workhorse for showing that a limit fails to exist, costs no choice principle at all.

• This is the standard way a limit is shown not to exist, and the reason is that the direct route would have to refute a statement beginning "there exists $L$": one would have to argue about every real $L$ at once. Two sequences reduce that to a single computation, as on the companion page for $\psi(1/x)$ at $0$ and for the indicator of $\mathbb{Q}$ at every point.

• The hypothesis "all terms in $A \setminus \{c\}$" is not decorative. A sequence allowed to take the value $c$ carries information about $f(c)$, which The $\varepsilon$-$\delta$ limit $\lim_{x \to c} f(x) = L$ of $f : A \to \mathbb{R}$ at a limit point $c$ of $A$ deliberately ignores; the constant sequence $z_k = c$ would then refute every limit at once.

• What the corollary does not say. It gives a sufficient condition for the limit not to exist, not a necessary one in any weaker form: the converse statement, that a limit exists as soon as all such image sequences converge to one value, is the other direction of Heine criterion: $\lim_{x \to c} f(x) = L$ iff $f(x_k) \to L$ for every sequence in $A \setminus \{c\}$ converging to $c$ and is exactly the direction that spends countable choice (The sequence-to-$\varepsilon$ direction of the Heine criterion uses countable choice for $\mathbb{R}$, and where this library records that cost).