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.
Finite-dimensional vector space, and its dimension ; infinite-dimensional means having no finite basis
Definition
Let be a vector space over a field (Vector space over a field).
is finite-dimensional over when it has a finite basis (Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis, Finite, countably infinite, countable, uncountable): some basis of satisfies for some (Equinumerous sets, and ).
For such a , the dimension of over , written , is that :
This is well defined. Existence of such an is the hypothesis, together
with the fact that a finite set is equinumerous with exactly one natural number
(The pigeonhole principle on , claim 3). Uniqueness is
If has a basis with elements and a basis with elements then ; and if has one finite basis then every basis of is finite: two bases of with and
with elements force . That theorem is therefore a prerequisite of
this definition, not a later justification of it, and it is listed in deps.
is infinite-dimensional over when it is not finite-dimensional over , that is, when has no finite basis. No number is attached to such a space here: the symbol is defined only in the finite-dimensional case, and the expression is not used.
The zero space. is a basis of (Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis) and , so is finite-dimensional with . Conversely a space of dimension has a basis , that is , and then (Linear combination of a finite list, and the span as the smallest linear subspace containing ).
Remarks
-
The subscript is not ornamental. By A field is a vector space over itself, and over any subfield every -vector space is a -vector space by restricting the scalars the same set with the same addition is a vector space over any subfield (Subfield: a subring of a field closed under inverses of its nonzero elements, and therefore a field with the restricted operations), and for a proper subfield the two structures can have different bases and different dimensions. The companion page's basis of over is the extreme case: is a vector space both over itself and over the embedded copy of inside it, and it is infinite-dimensional over the latter. So "the dimension of " is incomplete language in exactly the way that "the vector space " is, and both the space and the field are part of the statement of every result below.
-
Infinite-dimensional is defined as a negation, deliberately. Assigning a size to an infinite basis would require knowing that any two infinite bases of a space are equinumerous, which If has a basis with elements and a basis with elements then ; and if has one finite basis then every basis of is finite does not prove and this page does not claim; the standard argument for it is cardinal arithmetic, developed much later in the library. The companion page therefore records a proper subspace with an equinumerous basis rather than any statement of the form for infinite-dimensional spaces.
-
Dimension counts a basis, not a spanning set and not an independent set. A spanning set may be larger than and an independent set smaller; 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 is what bounds the second by the first, and For the following are equivalent: is a basis; is a maximal linearly independent subset of ; is a minimal spanning subset of — maximality and minimality being in the inclusion order is what says a basis is exactly where the two meet.
Depends on
If has a basis with elements and a basis with elements then ; and if has one finite basis then every basis of is finite
Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis
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
A field is a vector space over itself, and over any subfield every -vector space is a -vector space by restricting the scalars
Subfield: a subring of a field closed under inverses of its nonzero elements, and therefore a field with the restricted operations
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)