LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

For $B \subseteq 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

Statement

Let $V$ be a vector space over a field $F$ (Vector space over a field). Let $\mathcal{I}$ be the set of linearly independent subsets of $V$ (Linear independence: a finite list $v : n \to V$ is independent when $\sum_{i<n} \lambda_i v_i = 0_V$ forces every $\lambda_i = 0_F$ , and a subset $S \subseteq V$ is independent when every injective finite list into $S$ is independent) and $\mathcal{S}$ the set of spanning subsets of $V$ (Linear combination of a finite list, and the span $\operatorname{span}(S)$ as the smallest linear subspace containing $S$ ), each partially ordered by inclusion (Partial order and partially ordered set). For $B \subseteq V$ the following are equivalent.

(a) $B$ is a basis of $V$ (Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis).
(b) $B$ is a maximal element of $(\mathcal{I}, \subseteq)$ (Maximal element and greatest element): $B$ is linearly independent, and no linearly independent $A \subseteq V$ satisfies $B \subsetneq A$ .
(c) $B$ is a minimal element of $(\mathcal{S}, \subseteq)$ : $B$ spans $V$ , and no spanning $A \subseteq V$ satisfies $A \subsetneq B$ .

Facts & Assumptions

Given: A field $F$ , a vector space $V$ over $F$ , and a subset $B \subseteq V$ .

[L1]

$B$ is a basis of $V$ when $B$ is linearly independent and $\operatorname{span}(B) = V$ (Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis).

[L2]

A subset $T \subseteq V$ is linearly dependent if and only if some $t \in T$ lies in $\operatorname{span}(T \setminus \{t\})$ (A subset $S \subseteq V$ is linearly dependent if and only if some $s \in S$ lies in $\operatorname{span}(S \setminus \{s\})$ ; and $\operatorname{span}(S)$ is already the set of linear combinations of INJECTIVE finite lists into $S$ ).

[L3]

If $A$ is linearly independent and $w \notin \operatorname{span}(A)$ , then $w \notin A$ and $A \cup \{w\}$ is linearly independent (If $S \subseteq V$ is linearly independent and $w \notin \operatorname{span}(S)$ then $S \cup \{w\}$ is linearly independent and $\operatorname{span}(S) \subsetneq \operatorname{span}(S \cup \{w\})$ ; and if $w \in \operatorname{span}(S)$ then $\operatorname{span}(S \cup \{w\}) = \operatorname{span}(S)$ ).

[L4]

Every subset of a linearly independent subset of $V$ is linearly 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, claim 7).

[L5]

$\operatorname{span}(T)$ is a linear subspace of $V$ containing $T$ and contained in every linear subspace of $V$ containing $T$ ; and $T \subseteq T'$ implies $\operatorname{span}(T) \subseteq \operatorname{span}(T')$ (Linear combination of a finite list, and the span $\operatorname{span}(S)$ as the smallest linear subspace containing $S$ , The span is monotone and idempotent, $\operatorname{span}(S) = S$ exactly when $S$ is a linear subspace, and $\operatorname{span}(S \cup \{0_V\}) = \operatorname{span}(S)$ , Linear subspace of a vector space).

[L6]

Inclusion is a partial order, and $m$ is maximal in a poset when no element is strictly above it, minimal when no element is strictly below it (Partial order and partially ordered set, Maximal element and greatest element).

Proof

technique · direct

1.1

(a) implies (b). Let $B$ be a basis, so $B$ is linearly independent and $\operatorname{span}(B) = V$ . Suppose some linearly independent $A$ satisfies $B \subsetneq A$ , and pick $w \in A \setminus B$ . Then $B \cup \{w\} \subseteq A$ , so $B \cup \{w\}$ is linearly independent. On the other hand $w \in V = \operatorname{span}(B)$ , and $B = (B \cup \{w\}) \setminus \{w\}$ because $w \notin B$ , so $B \cup \{w\}$ is linearly dependent. These contradict each other, so no such $A$ exists and $B$ is maximal in the inclusion order on the linearly independent subsets.

L1L2L4L6

1.2

(b) implies (a). Let $B$ be maximal among the linearly independent subsets of $V$ . If some $w \in V$ had $w \notin \operatorname{span}(B)$ , then $B \cup \{w\}$ would be linearly independent with $w \notin B$ , so $B \subsetneq B \cup \{w\}$ , contradicting maximality. Hence $V \subseteq \operatorname{span}(B)$ , and $\operatorname{span}(B) \subseteq V$ always, so $\operatorname{span}(B) = V$ and $B$ is a basis.

L1L3L5L6

1.3

(a) implies (c). Let $B$ be a basis, so $B$ spans $V$ . Suppose some spanning $A$ satisfies $A \subsetneq B$ , and pick $b \in B \setminus A$ . Then $A \subseteq B \setminus \{b\}$ , so $V = \operatorname{span}(A) \subseteq \operatorname{span}(B \setminus \{b\})$ by monotonicity, and in particular $b \in \operatorname{span}(B \setminus \{b\})$ . That makes $B$ linearly dependent, contradicting the assumption that $B$ is a basis. So $B$ is minimal among the spanning subsets.

L1L2L5L6

1.4

(c) implies (a). Let $B$ be minimal among the spanning subsets of $V$ , so $\operatorname{span}(B) = V$ . If $B$ were linearly dependent, there would be $b \in B$ with $b \in \operatorname{span}(B \setminus \{b\})$ ; then $\operatorname{span}(B \setminus \{b\})$ is a linear subspace of $V$ containing $B \setminus \{b\}$ and also containing $b$ , hence containing $B$ , hence containing $\operatorname{span}(B) = V$ by minimality of the span. So $B \setminus \{b\}$ spans $V$ while $B \setminus \{b\} \subsetneq B$ , contradicting minimality of $B$ . Hence $B$ is linearly independent and is a basis.

L1L2L5L6

2.1

Steps 1.1 and 1.2 give the equivalence of (a) and (b), and steps 1.3 and 1.4 give the equivalence of (a) and (c); so all three conditions are equivalent.

step 1.1step 1.2step 1.3step 1.4∎

Remarks

Maximal and minimal, never greatest and least. There is in general no largest independent subset and no smallest spanning subset: a space usually has many bases, pairwise incomparable under inclusion, and Maximal element and greatest element is explicit that maximality does not imply greatestness. The companion page exhibits a three-element spanning set of $F^{2}$ containing three different bases.
This is the lemma that converts an existence problem into an order problem. Producing a basis becomes producing a maximal element of a poset, which is what Zorn's lemma does (Zorn's lemma); producing one inside a given spanning set becomes the same problem in a smaller poset. Both are carried out in Zorn's lemma gives a basis between any linearly independent set and any spanning set containing it: if $L \subseteq S \subseteq V$ with $L$ independent and $\operatorname{span}(S) = V$ , there is a basis $B$ of $V$ with $L \subseteq B \subseteq S$ , whose poset is the one named in (b) above, cut down to the subsets lying between a given independent set and a given spanning set.
The two orders are the same order on different families. Nothing above compares an independent set with a spanning set; the maximality of (b) is taken inside $\mathcal{I}$ and the minimality of (c) inside $\mathcal{S}$ , and a basis is exactly a set that is extreme in both families at once.

Depends on

Used by

{(1,0), (0,1), (1,1)} spans F² and is linearly dependent, so a spanning set need not be a basis; each of its three two-element subsets is a basis Counterexample

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 59 results over 19 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Basis (linear algebra) (Wikipedia) (standard reference, not scraped)
S. Axler, Linear Algebra Done Right, 4th ed., Ch. 2 (standard reference, not scraped)
Cambridge University Press excerpt: Vector spaces and bases (standard reference, not scraped)

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