CounterexampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04

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.

Heine-Borel fails in ell^2

Statement refuted

Refuted claim: every closed and bounded subset of an infinite-dimensional Banach space is compact.

Take the Hilbert space

$ℓ^{2} : = {x = (x_{n})_{n \geq 0} : \sum_{n = 0}^{\infty} ∣ x_{n} ∣^{2} < \infty} .$

Its closed unit ball is closed and bounded, but it is not compact.

Facts & Assumptions

Given: The space $ℓ^{2}$ , its standard unit vectors $e_{n}$ , and its closed unit ball ${\overline{B}}_{ℓ^{2}}$ .

[L1]

In any normed space with no ordered basis of finite length, the closed unit ball is not compact (In an infinite-dimensional normed space the closed unit ball is not compact).

[L2]

The classical sequence spaces $ℓ^{p}$ are Banach; in particular $ℓ^{2}$ is Banach (The classical $L^{p}$ spaces are Banach spaces).

[L3]

A vector space with a finite spanning set has no linearly independent subset equinumerous with $N$ (If $V$ has a spanning set with $n$ elements, then every linearly independent subset of $V$ is finite with at most $n$ elements; in particular $V$ has no linearly independent subset equinumerous with $N$ ).

Counterexample

technique · direct

1.1

The standard unit vectors are linearly independent: if $\sum_{j = 0}^{m} a_{j} e_{j} = 0$ , then the $j$ -th coordinate of that sequence is $a_{j}$ , so every $a_{j} = 0$ . Therefore the set ${e_{n} : n \in N}$ is linearly independent and is equinumerous with $N$ . By [L3], $ℓ^{2}$ cannot be spanned by any finite list, hence it admits no ordered basis of finite length. Each $e_{n}$ belongs to $ℓ^{2}$ and has norm $1$ , so every $e_{n}$ lies in the closed unit ball. Also for $m \neq n$ one has $∥ e_{n} - e_{m} ∥_{2} = \sqrt{2}$ .

L3givenalgebra

2.1

By [L2], $ℓ^{2}$ is a Banach space. Since step 1.1 shows that $ℓ^{2}$ admits no ordered basis of finite length, [L1] implies that ${\overline{B}}_{ℓ^{2}}$ is not compact. This closed unit ball is closed and bounded by definition, so it refutes the claim.

L1L2step 1.1∎

Remarks

The Banach-space adjective in the refuted claim is there because the failure is not an incompleteness issue. The obstruction is infinite dimension.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

19 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

Gerald Teschl, Topics in Real and Functional Analysis (standard reference, not scraped)
Andrew Lin and Casey Rodriguez, MIT 18.102 Introduction to Functional Analysis (standard reference, not scraped)