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 finite-dimensional vector space over an infinite field is not a finite union of proper subspaces
Statement
Let be a finite-dimensional vector space over an infinite field . No finite family of proper linear subspaces of has union .
Facts & Assumptions
Given: A finite-dimensional vector space over an infinite field , and a finite family of proper linear subspaces.
A vector space has addition and scalar multiplication satisfying the vector-space axioms (Vector space over a field).
A finite-dimensional vector space has a finite basis, and the empty basis occurs exactly for the zero space (Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis).
A finite set has a natural-number cardinality invariant under bijection (The cardinality of a finite set).
Proof
For , the union is empty and cannot equal the nonempty set , even when is the zero space.
Assume the assertion for families of fewer than proper subspaces, in every finite-dimensional vector space over .
If , choose and the result is immediate. For , remove any contained in another member; if this shortens the family, the induction hypothesis applies. Otherwise every is a proper subspace of , so the induction hypothesis inside gives a nonzero lying in none of the earlier . Choose .
In the unresolved case , on the affine line each contains at most one point: two such points would have difference a nonzero scalar multiple of , putting in for , while any point in would put there.
For the union therefore meets the line in at most a finite set of points by [L3], whereas is injective and is infinite. Some point of the line lies outside every ; together with the conclusion in step 2.1, this completes the induction.
Depends on
Used by
- General hypersurfaces give smooth complete intersections Corollary
- Positive restricted roots and nilpotent n algebra Definition
- Satake diagram Definition
- Vogan diagram Definition
- A finite extension with only finitely many intermediate fields is simple Lemma
- Regular hyperplane step for coherent support induction Lemma
- The eventual Hilbert function of a zero-dimensional projective quotient equals its total length Lemma
- Cayley transforms connect theta-stable Cartans in the classification Theorem
- Classification of real forms by Vogan diagrams Theorem
- Conjugacy of maximal tori Theorem
- Maximal abelian subspaces of p are conjugate by K Theorem
- Rank-two root-system classification Theorem
Dependency tree · two levels
23 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
- P. L. Clark, Field Theory, Chapter 5 (standard reference, not scraped)
- J. S. Milne, Fields and Galois Theory, Chapter 5 (standard reference, not scraped)