TheoremStatement: AI-adaptedProof: AI-adaptedprecheck 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.

$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

Statement

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

$f$ is continuous at $c$ (Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point).
For every sequence $(x_{k})_{k \in 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 $(f (x_{k}))_{k \in 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 ∖ {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 ∖ {c}$ converging to $c$ , and therefore inherits the one use of the axiom of countable choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )) 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- $ε$ direction of the Heine criterion uses countable choice for $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 $ε$ and $δ$ , 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.

Facts & Assumptions

Given: A set $A \subseteq R$ , a function $f : A \to R$ and a point $c \in A$ .

[L1]

Continuity at $c$ : for every real $ε > 0$ there is a real $δ > 0$ such that every $x \in A$ with $∣ x - c ∣ < δ$ satisfies $∣ f (x) - f (c) ∣ < ε$ (Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point).

[L2]

A point of $A$ is either a limit point of $A$ or an isolated point of $A$ , and never both; $c$ is isolated in $A$ when $N_{η} (c) \cap A = {c}$ for some real $η > 0$ (Limit point, isolated point, adherent point, derived set, and dense subset of $R$ , The $ε$ -neighbourhood and the punctured $ε$ -neighbourhood of a point of $R$ ).

[L3]

At a limit point $c$ of $A$ , $f$ is continuous at $c$ if and only if the limit of $f$ at $c$ exists and equals $f (c)$ ; at an isolated point of $A$ every function is continuous (Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point, The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ ).

[L4]

Heine criterion for limits: at a limit point $c$ of $A$ , $\lim_{x \to c} f (x) = L$ holds if and only if $f (x_{k}) \to L$ for every sequence $(x_{k})$ with $x_{k} \in A$ , $x_{k} \neq c$ for every $k$ , and $x_{k} \to c$ . The direction from the limit to sequences is a theorem of ZF; the converse uses the axiom of countable choice exactly once (Heine criterion: $\lim_{x \to c} f (x) = L$ iff $f (x_{k}) \to L$ for every sequence in $A ∖ {c}$ converging to $c$ , The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[L5]

Convergence of a real sequence: $x_{k} \to x$ when for every rational $ε > 0$ there is $K$ with $∣ x_{k} - x ∣ < ε$ for all $k \geq K$ ; below every positive real lies a positive rational, so the test may equally be run at every real $ε > 0$ (Limits and Cauchy sequences of reals, Sequences of reals: bounded, eventually, frequently, tails, subsequences, The rationals embed densely in the reals).

[L6]

Absolute value: $∣ u ∣ \geq 0$ , and $∣ u ∣ = 0$ exactly when $u = 0$ (Basic properties of the absolute value).

Proof

technique · direct

1.1

The isolated case, both statements at once. Suppose $c$ is an isolated point of $A$ and fix a real $η > 0$ with $N_{η} (c) \cap A = {c}$ . Then statement 1 holds by [L3]. Statement 2 also holds: if $x_{k} \in A$ for every $k$ and $x_{k} \to c$ , then by [L5] there is $K$ with $∣ x_{k} - c ∣ < η$ for all $k \geq K$ , so $x_{k} \in N_{η} (c) \cap A = {c}$ and hence $x_{k} = c$ and $f (x_{k}) = f (c)$ for all $k \geq K$ ; a sequence eventually equal to $f (c)$ converges to $f (c)$ , since $∣ f (x_{k}) - f (c) ∣ = 0 < ε$ for $k \geq K$ . So 1 and 2 are both true, and in particular equivalent.

L2L3L5L6

1.2

The limit-point case, from 1 to 2. Suppose $c$ is a limit point of $A$ and that $f$ is continuous at $c$ . Let $(x_{k})$ satisfy $x_{k} \in A$ for every $k$ and $x_{k} \to c$ , and let a rational $ε > 0$ be given. By [L1] fix a real $δ > 0$ with $∣ f (x) - f (c) ∣ < ε$ for every $x \in A$ satisfying $∣ x - c ∣ < δ$ ; by [L5] fix $K$ with $∣ x_{k} - c ∣ < δ$ for all $k \geq K$ . Every such $k$ has $x_{k} \in A$ and $∣ x_{k} - c ∣ < δ$ , hence $∣ f (x_{k}) - f (c) ∣ < ε$ . As the rational $ε > 0$ was arbitrary, $f (x_{k}) \to f (c)$ . Nothing was selected, so this is a theorem of ZF.

L1L5

1.3

The limit-point case, from 2 to 1. Suppose $c$ is a limit point of $A$ and that statement 2 holds. Every sequence $(x_{k})$ with $x_{k} \in A$ , $x_{k} \neq c$ for every $k$ , and $x_{k} \to c$ is in particular a sequence in $A$ converging to $c$ , so statement 2 gives $f (x_{k}) \to f (c)$ . That is the right-hand side of [L4] with $L : = f (c)$ , so [L4] yields that the limit of $f$ at $c$ exists and equals $f (c)$ , and [L3] turns that into continuity of $f$ at $c$ . This is the direction that inherits the single use of countable choice made in [L4].

L3L4

2.1

By [L2] the point $c$ is either isolated in $A$ or a limit point of $A$ . In the first case step 1.1 proves both statements outright; in the second, step 1.2 gives 1 implies 2 and step 1.3 gives 2 implies 1. So statements 1 and 2 are equivalent, with the first implication free of choice and the second inheriting exactly one application of countable choice.

step 1.1step 1.2step 1.3L2∎

Remarks

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 ∖ {c}$ converging to $c$ must exclude $c$ , because The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to 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 ∖ {c}$ converging to $c$ . No claim is made that it is necessary; The sequence-to- $ε$ direction of the Heine criterion uses countable choice for $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 $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 $Q$ is continuous at no point of $R$ ↗ on the companion page is proved without sequences at all, directly from density, which is cheaper still.

Depends on

Used by

Dependency tree · two levels

39 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Continuous 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.2 (standard reference, not scraped)

ff is continuous at c∈Ac∈A if and only if f(xk)→f(c)f(xk​)→f(c) for every sequence in AA converging to cc, the converse direction costing countable choice