$f$ is continuous at $c \in A$ if and only if $f(x_k) \to f(c)$ for every sequence in $A$ converging to $c$, the converse direction costing countable choice

Let $A \subseteq \mathbb{R}$, let $f : A \to \mathbb{R}$ and let $c \in A$. The following are equivalent.

1. $f$ is continuous at $c$ (Continuity of $f : A \to \mathbb{R}$ at a point of $A$ and on $A$: the $\varepsilon$-$\delta$ condition, its agreement with $\lim_{x \to c} f(x) = f(c)$ at a limit point, and continuity at an isolated point).
2. For every sequence $(x_k)_{k \in \mathbb{N}}$ with $x_k \in A$ for every $k$ and $x_k \to c$ (Sequences of reals: bounded, eventually, frequently, tails, subsequences, Limits and Cauchy sequences of reals), the sequence $\bigl(f(x_k)\bigr)_{k \in \mathbb{N}}$ converges to $f(c)$.

The sequences here are not required to avoid $c$, which is the one difference from 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 what makes the criterion available at an isolated point of $A$, where no limit exists.

The two directions do not cost the same. The implication from 1 to 2 is proved in ZF: the sequence is handed to the proof and nothing is selected. The implication from 2 to 1 is obtained below from 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 therefore inherits the one use of the axiom of countable choice (The Axiom of Countable Choice ($\mathrm{AC}_\omega$)) made in that theorem's converse direction. What this library does and does not claim about that cost is recorded once, in The sequence-to-$\varepsilon$ direction of the Heine criterion uses countable choice for $\mathbb{R}$, and where this library records that cost, and is not restated here.

Nothing else on this page is routed through this theorem. The algebra of continuous functions, composition, the intermediate value theorem, the extreme value theorem and Heine-Cantor are all proved from $\varepsilon$ and $\delta$, or from compactness, exactly as the previous page organised itself. The choice-free direction 1 to 2 is used, in the intermediate value theorem and in Heine-Cantor, and each of those two items says which direction it uses.

• Why the sequences are allowed to hit $c$. 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$ must exclude $c$, because The $\varepsilon$-$\delta$ limit $\lim_{x \to c} f(x) = L$ of $f : A \to \mathbb{R}$ at a limit point $c$ of $A$ says nothing about $f(c)$ and a sequence constantly equal to $c$ would test the wrong thing. Continuity does look at $f(c)$, so no exclusion is needed, and dropping it is what makes statement 2 meaningful at an isolated point, where the only sequences converging to $c$ are those eventually equal to $c$.

• What the choice cost is, and what it is not. The claim recorded here is that the proof given above of 2 implies 1 uses countable choice, through 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$. No claim is made that it is necessary; The sequence-to-$\varepsilon$ direction of the Heine criterion uses countable choice for $\mathbb{R}$, and where this library records that cost states in full what this library does and does not assert, including Sierpiński's ZF theorem that a function continuous sequentially at every point of $\mathbb{R}$ is continuous, which shows the everywhere-statement and the pointwise statement behave differently.

• The negative use is the common one. To show that $f$ is not continuous at $c$ it suffices to exhibit one sequence in $A$ converging to $c$ whose image sequence does not converge to $f(c)$, and that uses only the choice-free direction. The indicator of $\mathbb{Q}$ is continuous at no point of $\mathbb{R}$ ↗ on the companion page is proved without sequences at all, directly from density, which is cheaper still.