LemmaStatement: AI-adaptedProof: AI-adaptedprecheck 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 R$ (Sequences of reals: bounded, eventually, frequently, tails, subsequences, Limits and Cauchy sequences of reals), and let $n : N \to 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 : N \to 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 $ε > 0$ there is $K \in N$ with $∣ x_{k} - x ∣ < \hat{ε}$ for all $k \geq K$ (Limits and Cauchy sequences of reals).

[L2]

Growth of the index map: $n_{k} \geq k$ for every $k$ (A strictly increasing index map satisfies $n_{k} \geq k$ ).

[L3]

The order on $N$ is transitive, so $n_{k} \geq k \geq K$ gives $n_{k} \geq K$ ( $\leq$ is a linear order on $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 $ε > 0$ be rational. By convergence of $(x_{k})$ there is $K \in N$ with $∣ x_{j} - x ∣ < ε$ for every $j \geq K$ .

2.1

For every $k \geq K$ we have $n_{k} \geq k \geq K$ , so the estimate of step 1.1 applies at the index $j = n_{k}$ and gives $∣ x_{n_{k}} - x ∣ < ε$ .

step 1.1L2L3

3.1

Since the rational $ε > 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 \neq 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 · two levels

30 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

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)