LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passverified 2026-08-05 (gpt-5.6-sol-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.

Subsequences inherit the limit

Statement

Let $(x_k)$ be a sequence of reals converging to $x \in \mathbb{R}$ (Sequences of reals: bounded, eventually, frequently, tails, subsequences, Limits and Cauchy sequences of reals), and let $n : \mathbb{N} \to \mathbb{N}$ be strictly increasing. Then the subsequence $(x_{n_k})$ converges to $x$ .

Divergence test. Consequently, if two subsequences of $(x_k)$ converge to different limits, then $(x_k)$ does not converge.

Facts & Assumptions

Given: A sequence $(x_k)$ of reals converging to a real $x$ , and a strictly increasing $n : \mathbb{N} \to \mathbb{N}$ , so that $(x_{n_k})$ is a subsequence of $(x_k)$ (Sequences of reals: bounded, eventually, frequently, tails, subsequences, Limits and Cauchy sequences of reals).

[L1]

$(x_k)$ converges to $x$ when for every rational $\varepsilon > 0$ there is $K \in \mathbb{N}$ with $|x_k - x| < \hat\varepsilon$ for all $k \ge K$ (Limits and Cauchy sequences of reals).

[L2]

Growth of the index map: $n_k \ge k$ for every $k$ (A strictly increasing index map satisfies $n_k \ge k$ ).

[L3]

The order on $\mathbb{N}$ is transitive, so $n_k \ge k \ge K$ gives $n_k \ge K$ ( $\le$ is a linear order on $\mathbb{N}$ , Order on the natural numbers).

[L4]

A sequence has at most one limit (A sequence has at most one limit).

Proof

technique · direct

1.1

Let $\varepsilon > 0$ be rational. By convergence of $(x_k)$ there is $K \in \mathbb{N}$ with $|x_j - x| < \varepsilon$ for every $j \ge K$ .

2.1

For every $k \ge K$ we have $n_k \ge k \ge K$ , so the estimate of step 1.1 applies at the index $j = n_k$ and gives $|x_{n_k} - x| < \varepsilon$ .

step 1.1L2L3

3.1

Since the rational $\varepsilon > 0$ was arbitrary, and the same threshold $K$ served, $(x_{n_k})$ converges to $x$ .

step 2.1L1

4.1

Divergence test: suppose subsequences $(x_{n_k})$ and $(x_{m_k})$ converge to $a$ and $b$ with $a \ne b$ . If $(x_k)$ converged, to $x$ say, then by step 3.1 both subsequences would converge to $x$ , and uniqueness of limits would force $a = x$ and $b = x$ , hence $a = b$ , contrary to hypothesis; so $(x_k)$ does not converge.

step 3.1L4∎

Remarks

A sequence is a subsequence of itself, via the identity index map $n_k = k$ , which is strictly increasing. So "every subsequence converges to $x$ " and "the sequence converges to $x$ " are equivalent, and the lemma is the non-trivial half of that equivalence.
The converse of the first claim is false: one convergent subsequence says nothing about the sequence (FALSE: a convergent subsequence forces the sequence to converge). It is the divergence test, not the convergence of a single subsequence, that is usable.
The divergence test is the standard way to show a concrete sequence diverges, and it is how FALSE: every bounded sequence converges is refuted. The opposite direction, extracting a convergent subsequence from a bounded sequence, is Bolzano-Weierstrass; it is not available at this point in the reading order, being the subject of the next page of this track, Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness, where it is proved.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 53 results over 13 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. K. Hunter, An Introduction to Real Analysis, Ch. 3 (standard reference, not scraped)
CMU 21-269 notes, Compactness — subsequences (standard reference, not scraped)
Subsequence (Wikipedia) (standard reference, not scraped)
Limit of a sequence (Wikipedia) (standard reference, not scraped)
T. Tao, Analysis I, 3rd ed., §6.6 (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 3 (standard reference, not scraped)