Linear Independence, Bases and Dimension

About this page

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.

✓ 17 results · all verified · 16 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

1 · Prerequisites

Abstract Algebra

Linear Algebra

Vector Spaces, Linear Subspaces, Span and Direct Sums

Real Analysis

Set Theory

2 · Logical flowchart

3 · Items

Linear independence: a finite list v : n → V is independent when ∑_i<n λᵢ vᵢ = 0_V forces every λᵢ = 0_F, and a subset S ⊆ V is independent when every injective finite list into S is independent

Finite sums re-indexed along an injection, with a zero term deleted, and concatenated; and the closure properties of linear independence: an independent list is injective and never 0_V, its sublists are independent, a list is independent exactly when it is injective with linearly independent image, and every subset of a linearly independent set is linearly independent

A subset S ⊆ V is linearly dependent if and only if some s ∈ S lies in span(S ∖ {s}); and span(S) is already the set of linear combinations of INJECTIVE finite lists into S

S ⊆ V is linearly independent if and only if every finite subset of S is; consequently the union of a nonempty chain of linearly independent subsets of V, ordered by inclusion, is linearly independent

If S ⊆ V is linearly independent and w ∉ span(S) then S ∪ {w} is linearly independent and span(S) ⊊ span(S ∪ {w}); and if w ∈ span(S) then span(S ∪ {w}) = span(S)

Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis

A finite list v : n → V is an ordered basis if and only if every x ∈ V equals ∑_i<n λᵢ vᵢ for exactly one λ : n → F; those scalars are the coordinates of x in that ordered basis

For B ⊆ V the following are equivalent: B is a basis; B is a maximal linearly independent subset of V; B is a minimal spanning subset of V — maximality and minimality being in the inclusion order

The Steinitz exchange lemma: if L ⊆ V is linearly independent and S ⊆ V spans V with S finite of size n, then L is finite with |L| = m ≤ n, and there is T ⊆ S of size n - m such that L ∪ T spans V

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 ℕ

If V has a basis with n elements and a basis with m elements then n = m; and if V has one finite basis then every basis of V is finite

Finite-dimensional vector space, and its dimension dim_F V; infinite-dimensional means having no finite basis

Zorn's lemma gives a basis between any linearly independent set and any spanning set containing it: if L ⊆ S ⊆ V with L independent and span(S) = V, there is a basis B of V with L ⊆ B ⊆ S

Every spanning subset of a vector space contains a basis

Every vector space has a basis

The standard list e : n → Fⁿ with eᵢ(i) = 1_F and eᵢ(j) = 0_F for j ≠ i is an ordered basis of Fⁿ; hence dim_F Fⁿ = n, and F⁰ is the zero space with basis ∅ and dimension 0

If dim_F V = n and U is a linear subspace of V, then U is finite-dimensional, dim_F U ≤ n, and dim_F U = n if and only if U = V

Every linear subspace U of a vector space V has a complement: a linear subspace W with V = U ⊕ W

The dimension formula: for finite-dimensional linear subspaces U and W of V, the subspaces U + W and U ∩ W are finite-dimensional and dim_F(U+W) + dim_F(U ∩ W) = dim_F U + dim_F W

If V = ⨁_i<n Uᵢ with every Uᵢ finite-dimensional, then V is finite-dimensional and dim_F V = ∑_i<n dim_F Uᵢ; in particular dim_F(U ⊕ W) = dim_F U + dim_F W

Sources