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 be a sequence of reals converging to (Sequences of reals: bounded, eventually, frequently, tails, subsequences, Limits and Cauchy sequences of reals), and let be strictly increasing. Then the subsequence converges to .
Divergence test. Consequently, if two subsequences of converge to different limits, then does not converge.
Facts & Assumptions
Given: A sequence of reals converging to a real , and a strictly increasing , so that is a subsequence of (Sequences of reals: bounded, eventually, frequently, tails, subsequences, Limits and Cauchy sequences of reals).
converges to when for every rational there is with for all (Limits and Cauchy sequences of reals).
Growth of the index map: for every (A strictly increasing index map satisfies ).
The order on is transitive, so gives ( is a linear order on , Order on the natural numbers).
A sequence has at most one limit (A sequence has at most one limit).
Proof
Let be rational. By convergence of there is with for every .
For every we have , so the estimate of step 1.1 applies at the index and gives .
Since the rational was arbitrary, and the same threshold served, converges to .
Divergence test: suppose subsequences and converge to and with . If converged, to say, then by step 3.1 both subsequences would converge to , and uniqueness of limits would force and , hence , contrary to hypothesis; so does not converge.
Remarks
-
A sequence is a subsequence of itself, via the identity index map , which is strictly increasing. So "every subsequence converges to " and "the sequence converges to " 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.