ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passaudited 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.

A choice-free discontinuous linear functional on c_00

Example

Let

$c_{00} : = {x = (x_{n})_{n \geq 0} : x_{n} = 0 for all but finitely many n}$

with the supremum norm $∥ x ∥_{\infty} : = \sup_{n} ∣ x_{n} ∣$ , a norm in the sense of A norm on a real vector space, the induced metric, and the dictionary with the metric axioms. Define

$f : c_{00} \to R, f (x) : = \sum_{n = 0}^{\infty} (n + 1) x_{n} .$

Because every $x \in c_{00}$ has finite support, the displayed sum is really finite. The map $f$ is linear but unbounded, hence discontinuous.

Facts & Assumptions

Given: The space $c_{00}$ with its supremum norm and the standard unit vectors $e_{n}$ .

[L1]

Linearity means preserving scalar combinations (Linear map between vector spaces over the same field).

[L2]

A normed space is a vector space equipped with a norm (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms).

Verification

technique · direct

1.1

Because every element of $c_{00}$ has finite support, the displayed sum for $f (x)$ has only finitely many nonzero terms. Therefore $f$ is well defined, and termwise addition shows $f (a x + b y) = a f (x) + b f (y)$ for all scalars $a, b$ and all $x, y \in c_{00}$ . Thus $f$ is linear by [L1].

L1L2algebra

2.1

For each $n$ , the unit vector $e_{n}$ satisfies $∥ e_{n} ∥_{\infty} = 1$ and $f (e_{n}) = n + 1$ . Hence the values of $f$ on the unit sphere are unbounded, so no constant $C$ can satisfy $∣ f (x) ∣ \leq C ∥ x ∥_{\infty}$ for all $x \in c_{00}$ . Thus $f$ is unbounded.

step 1.1algebra

3.1

Every bounded linear functional on a normed space is continuous at $0$ , so an unbounded linear functional cannot be continuous. Therefore $f$ is a discontinuous linear functional on $c_{00}$ .

step 2.1assume-contradischarge-contradiction∎

Remarks

This is the explicit incomplete-space witness promised by the companion remark. No choice principle is used anywhere in the construction.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

16 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

Christopher Heil, A Basis Theory Primer (standard reference, not scraped)