The sequence-to-$\varepsilon$ direction of the Heine criterion uses countable choice for $\mathbb{R}$, and where this library records that cost

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$ is an equivalence, and its two directions do not cost the same.

• From the $\varepsilon$-$\delta$ limit to sequences — if $\lim_{x \to c} f(x) = L$ then $f(x_k) \to L$ for every sequence in $A \setminus \{c\}$ tending to $c$ — is proved in ZF. The sequence is handed to the proof; nothing is selected. This is steps 1.1, 2.1 and 3.1 of that theorem.

• From sequences to the $\varepsilon$-$\delta$ limit is proved there using the Axiom of Countable Choice (The Axiom of Countable Choice ($\mathrm{AC}_\omega$)), invoked exactly once, at step 3.2. The proof assumes the limit fails, obtains for each $k \in \mathbb{N}$ a nonempty set $X_k = \{\, x \in A : 0 < |x - c| < 1/(k+1) \text{ and } |f(x) - L| \ge \varepsilon_0 \,\}$, and needs a single point from each of those countably many sets at once.

Why no canonical selection is available. The sets $X_k$ are cut out by an inequality involving $f$, about which the theorem assumes nothing. There is therefore no rule in this library that names an element of $X_k$ uniformly in $k$: they are subsets of $\mathbb{R}$, which carries no well-ordering that ZF provides, and the sets need not be intervals, need not be closed, and need not meet $\mathbb{Q}$. That is precisely the situation The Axiom of Countable Choice ($\mathrm{AC}_\omega$) exists for.

The identical pattern occurs in the prerequisite page: in A point lies in the closure of $A \subseteq \mathbb{R}$ iff some sequence in $A$ converges to it, so a subset of $\mathbb{R}$ is closed iff it is sequentially closed the right-to-left direction is choice free, while producing a sequence in $A$ converging to a point of $\overline{A}$ requires selecting one point of $A$ from each of the sets $N_{1/(k+1)}(x) \cap A$, and that item invokes $\mathrm{AC}_\omega$ explicitly for it. Both items name the step where the axiom is used, so a reader working in ZF alone can see exactly which half of each equivalence survives.

• Claimed: the direction from $\varepsilon$-$\delta$ to sequences is a theorem of ZF; the converse as proved here uses $\mathrm{AC}_\omega$; and the use is isolated to one step, so nothing else on this page inherits it.

• Not claimed: that the converse requires $\mathrm{AC}_\omega$. This library proves no independence result and contains neither forcing nor permutation models, so it is in no position to assert that some cleverer ZF proof does not exist. The systematic study of which such criteria need which fragment of choice is a subject in its own right; Herrlich's Axiom of Choice is the standard reference, and it is cited here as literature, not used.

• A warning against a tempting slogan. It is not the case that sequential criteria in analysis always need choice. Sierpiński proved, in ZF, that a function $\mathbb{R} \to \mathbb{R}$ which is sequentially continuous at every point is continuous. The everywhere-statement and the pointwise-statement behave differently, and the cost recorded above is a statement about the pointwise criterion as proved here, nothing more.

Because the criterion carries a choice cost on one side, this page does not route its main results through it. The algebra of limits (Sums, scalar multiples, products and quotients of function limits, the quotient under the hypothesis that the denominator limit is nonzero), order preservation (If $f \le g$ on a punctured neighbourhood of $c$ then $\lim f \le \lim g$, non-strictly), the squeeze theorem (If $f \le g \le h$ near $c$ and $f$ and $h$ have the same limit at $c$, then so does $g$) and composition (Composition of limits holds under either hypothesis: $f$ is defined at $L$ with value $M$, or $g$ avoids $L$ on a punctured neighbourhood of $c$) are all proved directly from $\varepsilon$ and $\delta$, and are therefore theorems of ZF. The sequential machinery is used only where it earns its place: in the criterion itself, and in 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, which needs only the choice-free direction and is the tool by which the companion page shows that various limits fail to exist.

That organisation is a deliberate choice of proofs, not a mathematical necessity: each of those four results could be deduced from the criterion, at the price of importing $\mathrm{AC}_\omega$ into statements that do not need it.