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.
FALSE: a sequence in whose coordinate sequences are each bounded converges
Statement
False claim: let and let be a sequence in such that every coordinate sequence is bounded (Sequences of reals: bounded, eventually, frequently, tails, subsequences). Then converges in (Convergence of a sequence in a metric space: iff in , as the set of functions , and , , are metrics on it).
The claim conflates two theorems. What is true about boundedness is For every bounded sequence in has a convergent subsequence: a bounded sequence has a convergent subsequence. What is true componentwise is For a sequence in converges iff each coordinate sequence converges, is Cauchy iff each coordinate sequence is Cauchy, and is complete in every norm clause 1, which is about convergence of the coordinate sequences and says nothing about boundedness. The false claim takes the hypothesis of the first and the conclusion of the second.
The witness is the smallest possible. Take and let be the function with value at , where is the alternating sequence (The even and odd index maps and the alternating sequence: strictly increasing with their disjoint union, and the unique with , , which satisfies , and ).
Facts & Assumptions
Given: The alternating sequence , with , and ; its even and odd index maps and , strictly increasing with and for every (The even and odd index maps and the alternating sequence: strictly increasing with their disjoint union, and the unique with , , which satisfies , and ); and the sequence with .
The refuted claim, at and this sequence: converges in .
The alternating sequence and its index maps, and (The even and odd index maps and the alternating sequence: strictly increasing with their disjoint union, and the unique with , , which satisfies , and , Basic properties of the absolute value, A strictly increasing index map satisfies ).
Convergence in for is componentwise (For a sequence in converges iff each coordinate sequence converges, is Cauchy iff each coordinate sequence is Cauchy, and is complete in every norm clause 1, The standard list with and for is an ordered basis of ; hence , and is the zero space with basis and dimension , The -norms for rational , and , Each is a norm on , and the induced metrics are exactly , and of the published metric-spaces page, The finite and reverse triangle inequalities for a norm; and for every norm on satisfies and is Lipschitz, hence continuous, for ).
A subsequence of a convergent real sequence converges to the same limit, and a real sequence has at most one limit (Subsequences inherit the limit, A sequence has at most one limit, Limits and Cauchy sequences of reals).
A constant real sequence converges to its value (Limits and Cauchy sequences of reals).
A bounded sequence in has a convergent subsequence (For every bounded sequence in has a convergent subsequence, Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space, Isometry, isometric embedding, and the subspace metric on a subset); and a convergent real sequence is bounded (Every convergent sequence is bounded).
Refutation
The only coordinate sequence of is , and it is bounded: for every , so works. So the hypothesis of the refuted claim is met.
The subsequence is constantly and converges to ; the subsequence is constantly and converges to ; both index maps are strictly increasing.
The real sequence does not converge: if it converged to , both subsequences of step 1.2 would converge to , so and by uniqueness of limits, contradicting .
By the componentwise criterion, converges in if and only if converges in ; by step 2.1 it does not. So [A1] fails while the hypothesis holds, and the claim is false.
The true statement in this neighbourhood is that the sequence has a convergent subsequence: its range is bounded, so [L6] applies, and step 1.2 exhibits two convergent subsequences with different limits.
Remarks
-
The same witness separates the two notions on the real line. Boundedness of a real sequence gives a convergent subsequence and nothing more, and the alternating sequence has limit inferior and limit superior , so by A real sequence converges to iff , and diverges to iff both equal it cannot converge. That is a second route to step 2.1; the one taken above uses only uniqueness of limits.
-
Componentwise boundedness and boundedness agree, so nothing is gained by weakening the hypothesis. For the comparison chain (The finite and reverse triangle inequalities for a norm; and for every norm on satisfies and is Lipschitz, hence continuous, for clause 3) shows that a sequence in has bounded range if and only if every coordinate sequence is bounded. So the refuted claim is exactly the claim that a bounded sequence converges, restated coordinatewise.
-
The converse direction is fine. A convergent sequence in does have bounded coordinate sequences, each coordinate sequence being convergent by For a sequence in converges iff each coordinate sequence converges, is Cauchy iff each coordinate sequence is Cauchy, and is complete in every norm clause 1 and a convergent real sequence being bounded (Every convergent sequence is bounded). Only the direction asserted above fails.
Depends on
- For $n \ge 1$ every bounded sequence in $\mathbb{R}^n$ has a convergent subsequence
- For $n \ge 1$ a sequence in $\mathbb{R}^n$ converges iff each coordinate sequence converges, is Cauchy iff each coordinate sequence is Cauchy, and $\mathbb{R}^n$ is complete in every norm
- A sequence has at most one limit
- Subsequences inherit the limit
- A real sequence converges to $L \in \mathbb{R}$ iff $\liminf x_k = \limsup x_k = L$, and diverges to $\pm\infty$ iff both equal $\pm\infty$
- The even and odd index maps and the alternating sequence: strictly increasing $e, o$ with $\mathbb{N}$ their disjoint union, and the unique $(s_k)$ with $s_0 = 1$, $s_{\sigma(k)} = -s_k$, which satisfies $|s_k| = 1$, $s \circ e \equiv 1$ and $s \circ o \equiv -1$
- Convergence of a sequence in a metric space: $x_k \to x$ iff $d(x_k, x) \to 0$ in $\mathbb{R}$
- Sequences of reals: bounded, eventually, frequently, tails, subsequences
- Limits and Cauchy sequences of reals
- $\mathbb{R}^n$ as the set of functions $n \to \mathbb{R}$, and $d_1$, $d_2$, $d_\infty$ are metrics on it
- The $p$-norms $\lVert x\rVert_p$ for rational $p \ge 1$, and $\lVert x\rVert_\infty$
- The finite and reverse triangle inequalities for a norm; and for $n \ge 1$ every norm $N$ on $\mathbb{R}^n$ satisfies $N(x) \le C\lVert x\rVert_1$ and is Lipschitz, hence continuous, for $d_2$
- Each $\lVert\cdot\rVert_p$ is a norm on $\mathbb{R}^n$, and the induced metrics are exactly $d_1$, $d_2$ and $d_\infty$ of the published metric-spaces page
- Every convergent sequence is bounded
- The standard list $e : n \to F^{n}$ with $e_i(i) = 1_F$ and $e_i(j) = 0_F$ for $j \ne i$ is an ordered basis of $F^{n}$; hence $\dim_F F^{n} = n$, and $F^{0}$ is the zero space with basis $\varnothing$ and dimension $0$
- Isometry, isometric embedding, and the subspace metric on a subset
- Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space
- Canonical naturals are positive and strictly increasing
- The canonical natural $\iota(n) = n \cdot 1_F$ of a field
- A strictly increasing index map satisfies $n_k \ge k$
- Basic properties of the absolute value
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 218 results over 36 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
- Bolzano-Weierstrass theorem (Wikipedia) (standard reference, not scraped)
- Limit of a sequence (Wikipedia) (standard reference, not scraped)
- J. Demmel, MA221 Lecture 3: Vector Norms (standard reference, not scraped)
- G. Zitelli, Math 641 Functional Analysis, Part I (standard reference, not scraped)