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.
If has a spanning set with elements, then every linearly independent subset of is finite with at most elements; in particular has no linearly independent subset equinumerous with
Statement
Let be a vector space over a field (Vector space over a field) and suppose has a spanning subset (Linear combination of a finite list, and the span as the smallest linear subspace containing ) with for some (Equinumerous sets, and ). Then:
- every linearly independent subset (Linear independence: a finite list is independent when forces every , and a subset is independent when every injective finite list into is independent) is finite (Finite, countably infinite, countable, uncountable), and the unique with satisfies ;
- no linearly independent subset of is equinumerous with .
Facts & Assumptions
Given: A field , a vector space over , a spanning subset with , and a linearly independent subset .
Steinitz exchange: under these hypotheses is finite and the unique with satisfies (The Steinitz exchange lemma: if is linearly independent and spans with finite of size , then is finite with , and there is of size such that spans , claim 1).
A finite set is equinumerous with exactly one natural number, and for every (The pigeonhole principle on , claims 3 and 4).
is symmetric and transitive, being carried by bijections; and a set is finite when it is equinumerous with some natural number (Equinumerous sets, and , Injection, surjection, bijection, Finite, countably infinite, countable, uncountable, The natural numbers (von Neumann), Order on the natural numbers).
Proof
Claim 1 is exactly claim 1 of the Steinitz exchange lemma, whose hypotheses are the ones assumed here: spans and is finite of size , and is linearly independent.
Suppose some linearly independent satisfied . By claim 1 the set is finite, so for some ; by symmetry and transitivity of this gives , which is impossible.
Claim 1 is step 1.1 and claim 2 is step 1.2.
Remarks
-
Claim 2 is the form in which later items say a space is infinite-dimensional. Exhibiting a linearly independent subset equinumerous with shows, by this corollary read backwards, that the space has no finite spanning set at all, hence no finite basis. That is exactly the route taken on the companion page by the explicit infinite basis for the eventually zero families and by the independent set of that does not span it.
-
The bound is on the independent set, not on the spanning set. A spanning set may be enlarged freely without ceasing to span, so no bound in the other direction holds; what is bounded is how many vectors can be independent, and the bound is the size of any finite spanning set.
-
Nothing here assumes has a basis. The hypothesis is a finite spanning set, which need not be independent; that a spanning set contains a basis is Every spanning subset of a vector space contains a basis, proved later and by a different route.
Depends on
The Steinitz exchange lemma: if is linearly independent and spans with finite of size , then is finite with , and there is of size such that spans
Linear independence: a finite list is independent when forces every , and a subset is independent when every injective finite list into is independent
Linear combination of a finite list, and the span as the smallest linear subspace containing
Vector space over a field
Field
Finite, countably infinite, countable, uncountable
Equinumerous sets, and
Injection, surjection, bijection
The pigeonhole principle on
The natural numbers (von Neumann)
Order on the natural numbers