TheoremStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26

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.

A subset of $\mathbb{R}$ is compact iff it is sequentially compact

Statement

Let $K \subseteq \mathbb{R}$ . Then $K$ is compact if and only if $K$ is sequentially compact (Open cover, subcover, compact subset of $\mathbb{R}$ (every open cover has a finite subcover), and sequentially compact subset).

Neither implication is formal. Both are routed through the characterisation of compactness by closed and bounded (A subset of $\mathbb{R}$ is compact if and only if it is closed and bounded), and the forward implication additionally uses Bolzano-Weierstrass (Bolzano-Weierstrass: every bounded real sequence has a convergent subsequence). The backward implication uses the axiom of countable choice (The Axiom of Countable Choice ( $\mathrm{AC}_\omega$ )): twice, once inside 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 when a point of the closure is turned into a sequence, and once directly in step 2.3, where an unbounded set supplies one point beyond each natural bound.

Facts & Assumptions

Given: A subset $K \subseteq \mathbb{R}$ . Sequences are indexed by $\mathbb{N}$ , which contains $0$ (Sequences of reals: bounded, eventually, frequently, tails, subsequences).

[L1]

$K$ is compact when every open cover has a finite subcover, and sequentially compact when every sequence with all terms in $K$ has a subsequence converging to a point of $K$ (Open cover, subcover, compact subset of $\mathbb{R}$ (every open cover has a finite subcover), and sequentially compact subset, Subsequential limit of a real sequence, and the subsequential limit set, Limits and Cauchy sequences of reals).

[L2]

$K$ is compact exactly when $K$ is closed and bounded (A subset of $\mathbb{R}$ is compact if and only if it is closed and bounded).

[L3]

Bolzano-Weierstrass: a sequence $(x_k)$ of reals for which some $M$ satisfies $|x_k| \le M$ at every index has a subsequence converging to some real (Bolzano-Weierstrass: every bounded real sequence has a convergent subsequence).

[L4]

A point lies in $\overline{K}$ exactly when some sequence with all terms in $K$ converges to it, and $K$ is closed exactly when $\overline{K} = K$ , exactly when $K$ is sequentially closed (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, Interior, closure, boundary and exterior of a subset of $\mathbb{R}$ , Open subset of $\mathbb{R}$ (every point has a neighbourhood inside it), closed subset (complement open), and clopen).

[L5]

$K$ is bounded exactly when there are $\ell, u$ with $\ell \le y \le u$ for all $y \in K$ (Lower bound, bounded below, bounded set).

[L6]

Countable choice: for a family $(Y_k)_{k \in \mathbb{N}}$ of nonempty sets there is $f$ with domain $\mathbb{N}$ and $f(k) \in Y_k$ for every $k$ (The Axiom of Countable Choice ( $\mathrm{AC}_\omega$ )).

[L7]

A convergent sequence of reals is bounded (Every convergent sequence is bounded); every subsequence of a convergent sequence converges to the same limit (Subsequences inherit the limit); a sequence has at most one limit (A sequence has at most one limit); a strictly increasing $n : \mathbb{N} \to \mathbb{N}$ satisfies $n_j \ge j$ (A strictly increasing index map satisfies $n_k \ge k$ ).

[L8]

Archimedean property: for every real $z$ there is a natural $j \ge 1$ with $z < j$ ; canonical naturals satisfy $k \cdot 1_{\mathbb{R}} \ge 0$ and are increasing in $k$ (Every complete ordered field is Archimedean, Canonical naturals are positive and strictly increasing).

[L9]

Absolute value: $|z| \ge z$ , $|z| \ge -z$ , $|z| \ge 0$ , and $|z| = z$ for $z \ge 0$ while $|z| = -z$ for $z < 0$ (Basic properties of the absolute value).

[L10]

Every nonempty finite set of reals has a maximum, which is one of its members (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set).

Proof

technique · direct

1.1

For the forward implication assume $K$ is compact; then $K$ is closed and bounded by [L2], so [L5] supplies $\ell, u$ with $\ell \le y \le u$ for every $y \in K$ . Let $(x_k)$ be any sequence with $x_k \in K$ for every $k \in \mathbb{N}$ .

assume-hypL2L5

1.2

For the backward implication assume $K$ is sequentially compact.

assume-hypL1

2.1

The sequence of step 1.1 is bounded: put $M := \max\{|\ell|, |u|\}$ by [L10]; for each $k$ , from $\ell \le x_k \le u$ we get $x_k \le u \le |u| \le M$ and $-x_k \le -\ell \le |\ell| \le M$ , so $|x_k| \le M$ by [L9]. By [L3] there are a strictly increasing $n$ and a real $L$ with $x_{n_j} \to L$ ; every term $x_{n_j}$ lies in $K$ and $K$ is closed, so $L \in K$ by [L4]. Hence every sequence in $K$ has a subsequence converging in $K$ , that is, $K$ is sequentially compact.

step 1.1L1L3L4L9L10

2.2

A sequentially compact $K$ is closed: let $y \in \overline{K}$ ; by [L4] there is a sequence $(a_k)$ with $a_k \in K$ for all $k$ and $a_k \to y$ ; by sequential compactness some subsequence $(a_{n_j})$ converges to a point $z \in K$ ; but that subsequence also converges to $y$ by [L7], and limits are unique by [L7], so $z = y$ and $y \in K$ . Hence $\overline{K} \subseteq K$ , so $\overline{K} = K$ and $K$ is closed by [L4].

step 1.2L1L4L7

2.3

A sequentially compact $K$ is bounded: suppose it is not. Then for every $k \in \mathbb{N}$ the set $Y_k := \{\, y \in K : y > k \text{ or } y < -k \,\}$ is nonempty, since $Y_k = \varnothing$ would mean $-k \le y \le k$ for every $y \in K$ and make $K$ bounded by [L5]. Use [L6] to fix $f$ with $f(k) \in Y_k$ and put $x_k := f(k)$ ; then $x_k \in K$ , and $|x_k| > k$ for every $k$ , because $x_k > k \ge 0$ gives $|x_k| = x_k > k$ while $x_k < -k \le 0$ gives $|x_k| = -x_k > k$ by [L9] and [L8]. By sequential compactness some subsequence $(x_{n_j})$ converges, hence is bounded by some real $M$ with $|x_{n_j}| \le M$ for all $j$ by [L7]; by [L8] fix a natural $j \ge 1$ with $M < j$ , and then $|x_{n_j}| > n_j \ge j > M$ by [L7] and [L8], which contradicts $|x_{n_j}| \le M$ . So $K$ is bounded.

step 1.2L1L5L6L7L8L9

3.1

A sequentially compact $K$ is therefore closed by step 2.2 and bounded by step 2.3, hence compact by [L2].

step 2.2step 2.3L2

4.1

Step 2.1 is the forward implication and step 3.1 the backward one, so for subsets of $\mathbb{R}$ compactness and sequential compactness coincide.

step 2.1step 3.1∎

Remarks

The equivalence is proved, not defined, and it is proved through the order. Both directions pass through A subset of $\mathbb{R}$ is compact if and only if it is closed and bounded, whose backward half needs the completeness of $\mathbb{R}$ , and the forward direction adds Bolzano-Weierstrass: every bounded real sequence has a convergent subsequence, whose proof spends completeness again. Nothing here transfers to a setting where those are unavailable; see Which results on this page use the order of $\mathbb{R}$ and therefore have no general-topological analogue.
Where the choices are spent, and whether they can be avoided. Step 2.3 selects one point of $K$ outside $[-k,k]$ for each $k$ , and 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 selects one point of $K$ in each shrinking neighbourhood. Both are countably many independent selections from subsets of $\mathbb{R}$ , for which this library has no canonical rule, so The Axiom of Countable Choice ( $\mathrm{AC}_\omega$ ) is invoked rather than worked around. The forward implication, step 2.1, makes no such selection: the subsequence comes from Bolzano-Weierstrass: every bounded real sequence has a convergent subsequence as a single object.
Sequential compactness is the form used in analysis; compactness is the form that is stated without sequences. The extraction of a convergent subsequence is what proofs about continuous functions on $[a,b]$ actually use, while the covering definition mentions no sequence and no limit. This theorem is what lets a reader move between them for subsets of $\mathbb{R}$ , and it is proved only there.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 94 results over 25 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

Sequentially compact space (Wikipedia) (standard reference, not scraped)
Bolzano-Weierstrass theorem (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 2 and Ch. 3 (standard reference, not scraped)
J. Lebl, Basic Analysis I, §7.4 (standard reference, not scraped)
J. K. Hunter, An Introduction to Real Analysis (standard reference, not scraped)

A subset of R\mathbb{R}R is compact iff it is sequentially compact