TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passverified 2026-08-09 (gpt-5.6-terra-codex-subscription)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

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$

Statement

Let $A \subseteq \mathbb{R}$ , let $f : A \to \mathbb{R}$ , let $c$ be a limit point of $A$ (Limit point, isolated point, adherent point, derived set, and dense subset of $\mathbb{R}$ ) and let $L \in \mathbb{R}$ . The following are equivalent.

$\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$ ).
For every sequence $(x_k)_{k \in \mathbb{N}}$ with $x_k \in A$ and $x_k \ne c$ for every $k$ , and $x_k \to c$ (Sequences of reals: bounded, eventually, frequently, tails, subsequences, Limits and Cauchy sequences of reals), the sequence $(f(x_k))_{k \in \mathbb{N}}$ converges to $L$ .

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, as proved below, invokes the axiom of countable choice (The Axiom of Countable Choice ( $\mathrm{AC}_\omega$ )) exactly once, at step 3.2, to select one bad point from each of countably many nonempty sets. What this library does and does not claim about that cost is recorded in The sequence-to- $\varepsilon$ direction of the Heine criterion uses countable choice for $\mathbb{R}$ , and where this library records that cost; the same asymmetry appears, for the same reason, 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.

Because of this, the results on this page that can be proved directly from $\varepsilon$ and $\delta$ — the algebra of limits, order preservation, the squeeze theorem, composition — are proved that way, and not through this criterion. What the criterion is for is the transfer of sequential results to functions, and above all the negative use recorded 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.

Facts & Assumptions

Given: A set $A \subseteq \mathbb{R}$ , a function $f : A \to \mathbb{R}$ , a limit point $c$ of $A$ and a real $L$ . Sequences are functions on $\mathbb{N}$ , and $\mathbb{N}$ contains $0$ (Sequences of reals: bounded, eventually, frequently, tails, subsequences, The natural numbers $\mathbb{N}$ (von Neumann)), so the shrinking radii used below are $1/(k+1)$ and never $1/k$ .

[L1]

The function limit: $\lim_{x \to c} f(x) = L$ means that for every real $\varepsilon > 0$ there is a real $\delta > 0$ such that every $x \in A$ with $0 < |x - c| < \delta$ satisfies $|f(x) - L| < \varepsilon$ (The $\varepsilon$ - $\delta$ limit $\lim_{x \to c} f(x) = L$ of $f : A \to \mathbb{R}$ at a limit point $c$ of $A$ ).

[L2]

Sequential convergence: $(y_k) \to y$ means that for every rational $\varepsilon > 0$ there is $K \in \mathbb{N}$ with $|y_k - y| < \varepsilon$ for all $k \ge K$ (Limits and Cauchy sequences of reals, Sequences of reals: bounded, eventually, frequently, tails, subsequences). Testing instead against every positive REAL $\varepsilon$ defines the same relation: every positive rational is a positive real, and below every positive real lies a positive rational (The rationals embed densely in the reals), which is the passage sanctioned in the remarks of Sequences of reals: bounded, eventually, frequently, tails, subsequences.

[L3]

Limit point: for every real $\delta > 0$ there is $x \in A$ with $0 < |x - c| < \delta$ (Limit point, isolated point, adherent point, derived set, and dense subset of $\mathbb{R}$ , The $\varepsilon$ -neighbourhood and the punctured $\varepsilon$ -neighbourhood of a point of $\mathbb{R}$ ).

[L4]

Reciprocal Archimedean property: for every real $\varepsilon > 0$ there is a natural $n \ge 1$ with $1/n < \varepsilon$ (For every $\varepsilon > 0$ in a complete ordered field there is a natural $n \ge 1$ with $1/n < \varepsilon$ , Every complete ordered field is Archimedean); the canonical naturals satisfy $n \cdot 1_{\mathbb{R}} > 0$ and are strictly increasing in $n$ (Canonical naturals are positive and strictly increasing); and $0 < a < b$ gives $0 < 1/b < 1/a$ (Inverses of positives are positive, and reciprocation reverses order).

[L5]

Countable choice: for every family $(X_k)_{k \in \mathbb{N}}$ of nonempty sets there is a function $k \mapsto x_k$ with $x_k \in X_k$ for every $k$ (The Axiom of Countable Choice ( $\mathrm{AC}_\omega$ )).

[L6]

Absolute value (Basic properties of the absolute value); and trichotomy, so the negation of $|u| < \varepsilon$ is $|u| \ge \varepsilon$ , and the negation of "for every $\varepsilon$ there is $\delta$ such that P" is "there is $\varepsilon_0$ such that for every $\delta$ , not P" (Ordered field).

Proof

technique · direct

1.1

Assume condition 1, let $(x_k)$ be a sequence with $x_k \in A$ and $x_k \ne c$ for every $k$ and $x_k \to c$ , and let $\varepsilon > 0$ be an arbitrary real.

assume-hypL1L2L3

1.2

Assume condition 1 FAILS. Negating the quantifiers of [L1], there is a real $\varepsilon_0 > 0$ such that for every real $\delta > 0$ some $x \in A$ has $0 < |x - c| < \delta$ and $|f(x) - L| \ge \varepsilon_0$ .

assume-hypL1L6

2.1

By [L1] fix a real $\delta > 0$ such that every $x \in A$ with $0 < |x - c| < \delta$ satisfies $|f(x) - L| < \varepsilon$ ; and by [L2], $\delta$ being a positive real, fix $K \in \mathbb{N}$ with $|x_k - c| < \delta$ for every $k \ge K$ .

step 1.1L1L2choose

2.2

For $k \in \mathbb{N}$ put $X_k := \{\, x \in A \ : \ 0 < |x - c| < 1/(k+1) \ \text{ and } \ |f(x) - L| \ge \varepsilon_0 \,\}$ . Each $X_k$ is nonempty, since $k + 1 \ge 1$ makes $1/(k+1)$ a positive real and step 1.2 applies to that radius.

step 1.2L4L6

3.1

For every $k \ge K$ we have $x_k \in A$ and $x_k \ne c$ , so $0 < |x_k - c| < \delta$ and hence $|f(x_k) - L| < \varepsilon$ . Since $\varepsilon > 0$ was an arbitrary real, $f(x_k) \to L$ ; condition 1 therefore implies condition 2.

step 2.1L1L2L6

3.2

By countable choice applied to the family $(X_k)_{k \in \mathbb{N}}$ , fix a function $k \mapsto x_k$ with $x_k \in X_k$ for every $k \in \mathbb{N}$ .

step 2.2L5choose

4.1

That sequence has $x_k \in A$ and $x_k \ne c$ for every $k$ , and it converges to $c$ : given a real $\varepsilon > 0$ , [L4] supplies a natural $n \ge 1$ with $1/n < \varepsilon$ , and every $k \ge n$ has $k + 1 > n \ge 1$ , hence $|x_k - c| < 1/(k+1) < 1/n < \varepsilon$ .

step 3.2L2L4L6

4.2

Yet $(f(x_k))$ does not converge to $L$ : every $k$ has $|f(x_k) - L| \ge \varepsilon_0$ , while a rational $\varepsilon$ with $0 < \varepsilon < \varepsilon_0$ ([L2]) would require some $K$ with $|f(x_k) - L| < \varepsilon < \varepsilon_0$ for all $k \ge K$ .

step 3.2L2L6

5.1

So the failure of condition 1 produces a sequence witnessing the failure of condition 2; contrapositively, condition 2 implies condition 1, and with step 3.1 the two conditions are equivalent.

step 3.1step 4.1step 4.2∎

Remarks

Where the choice is spent, and where it is not. Step 3.2 is the only use of The Axiom of Countable Choice ( $\mathrm{AC}_\omega$ ) in this proof, and it occurs only in the direction from condition 2 to condition 1. Steps 1.1, 2.1 and 3.1, which prove the other direction, use no choice principle. The sequence-to- $\varepsilon$ direction of the Heine criterion uses countable choice for $\mathbb{R}$ , and where this library records that cost says what may and may not be concluded from that.
The sets $X_k$ genuinely have no canonical element. They are cut out by an inequality involving $f$ , about which nothing is assumed, so there is no rule in this library that picks a point of $X_k$ uniformly in $k$ . That is exactly the situation The Axiom of Countable Choice ( $\mathrm{AC}_\omega$ ) exists for, and it is the same situation as 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.
Why $1/(k+1)$ and not $1/k$ . Sequences here are functions on $\mathbb{N}$ and $\mathbb{N}$ contains $0$ (Sequences of reals: bounded, eventually, frequently, tails, subsequences), so the index $k = 0$ occurs and $1/k$ would be undefined there. The same convention is used 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.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 84 results over 28 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

J. Lebl, Basic Analysis I, §3.1: Limits of functions (standard reference, not scraped)
Limit of a function (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 4 (Thm 4.2) (standard reference, not scraped)
J. Lebl, Basic Analysis I, §3.1 (standard reference, not scraped)
Axiom of countable choice (Wikipedia) (standard reference, not scraped)

Heine criterion: lim⁡x→cf(x)=L\lim_{x \to c} f(x) = Llimx→c​f(x)=L iff f(xk)→Lf(x_k) \to Lf(xk​)→L for every sequence in A∖{c}A \setminus \{c\}A∖{c} converging to ccc