Alphabeta MathHow 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 finite-dimensional normed subspace is closed
Statement
Let be a normed space and let be a normed subspace. If admits an ordered basis of finite length, then is closed in .
Facts & Assumptions
Given: A normed space and a normed subspace that admits an ordered basis of finite length.
Such a normed space is Banach (Every finite-dimensional normed space is Banach).
A complete normed subspace is closed in the ambient normed space (A complete normed subspace is closed).
The restricted norm on a normed subspace is the ambient one (Normed subspace).
Proof
By [L3], the hypothesis makes a normed space in its own right, with an ordered basis of finite length. Therefore [L1] makes Banach, hence complete for its restricted norm.
Applying [L2] to that complete normed subspace shows that is closed in .
Depends on
Used by
- Under dependent choice, Riesz lemma builds an infinite separated sequence in the unit sphere Lemma
- A Banach space has no countably infinite Hamel basis Theorem
- A normed space is locally compact if and only if it is finite-dimensional Theorem
- The closed unit ball is compact if and only if the normed space is finite-dimensional Theorem
Dependency tree · two levels
12 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
- Daniel Daners, Introduction to Functional Analysis (standard reference, not scraped)