Alphabeta Math
CorollaryStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28
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 V has a spanning set with n elements, then every linearly independent subset of V is finite with at most n elements; in particular V has no linearly independent subset equinumerous with N

Statement

Let V be a vector space over a field F (Vector space over a field) and suppose V has a spanning subset S (Linear combination of a finite list, and the span span⁡(S) as the smallest linear subspace containing S) with S≈n for some n∈N (Equinumerous sets, A≈B and A⪯B). Then:

  1. every linearly independent subset L⊆V (Linear independence: a finite list v:n→V is independent when ∑i<nλivi=0V forces every λi=0F, and a subset S⊆V is independent when every injective finite list into S is independent) is finite (Finite, countably infinite, countable, uncountable), and the unique m∈N with L≈m satisfies m≤n;
  2. no linearly independent subset of V is equinumerous with N.

Facts & Assumptions

Given: A field F, a vector space V over F, a spanning subset S⊆V with S≈n, and a linearly independent subset L⊆V.

[L2]

A finite set is equinumerous with exactly one natural number, and N≉p for every p∈N (The pigeonhole principle on N, claims 3 and 4).

[L3]

≈ is symmetric and transitive, being carried by bijections; and a set is finite when it is equinumerous with some natural number (Equinumerous sets, A≈B and A⪯B, Injection, surjection, bijection, Finite, countably infinite, countable, uncountable, The natural numbers N (von Neumann), Order on the natural numbers).

Proof

technique · direct
1.1

Claim 1 is exactly claim 1 of the Steinitz exchange lemma, whose hypotheses are the ones assumed here: S spans V and is finite of size n, and L is linearly independent.

L1
1.2

Suppose some linearly independent L⊆V satisfied L≈N. By claim 1 the set L is finite, so L≈m for some m∈N; by symmetry and transitivity of ≈ this gives N≈m, which is impossible.

L1L2L3
2.1

Claim 1 is step 1.1 and claim 2 is step 1.2.

step 1.1step 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 N 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 FN 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 V 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

Used by

Dependency tree · two levels

45 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