LemmaStatement: AI-adaptedProof: AI-generatedSession-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.

The intersection of a nonempty family of linear subspaces of $V$ is a linear subspace of $V$

Statement

Let $V$ be a vector space over a field $F$ (Vector space over a field) and let $\mathcal{W}$ be a nonempty set of linear subspaces of $V$ (Linear subspace of a vector space). Then

$U \;=\; \bigcap_{W \in \mathcal{W}} W \;=\; \{\, x \in V \;:\; x \in W \text{ for every } W \in \mathcal{W} \,\}$

is a linear subspace of $V$ . In particular the intersection of two linear subspaces is a linear subspace.

Facts & Assumptions

Given: A field $F$ , a vector space $V$ over $F$ , a nonempty set $\mathcal{W}$ of linear subspaces of $V$ , and $U$ the intersection of the members of $\mathcal{W}$ .

[L1]

Each $W \in \mathcal{W}$ contains $0_V$ , is closed under $+$ , and is closed under scalar multiplication (Linear subspace of a vector space).

[L2]

One-step test: a nonempty $S \subseteq V$ with $\lambda u + v \in S$ for all $\lambda \in F$ and $u, v \in S$ is a linear subspace of $V$ (One-step subspace test: a nonempty $W \subseteq V$ is a linear subspace if and only if $\lambda u + v \in W$ for all $\lambda \in F$ and $u, v \in W$ ).

Proof

technique · direct

1.1

$U \subseteq V$ , since $\mathcal{W}$ is nonempty and every member of it is a subset of $V$ .

givenL1

1.2

$0_V \in U$ , since $0_V \in W$ for every $W \in \mathcal{W}$ ; in particular $U$ is nonempty.

1.3

Let $\lambda \in F$ and $u, v \in U$ , and let $W \in \mathcal{W}$ be arbitrary. Then $u, v \in W$ , so $\lambda u \in W$ by closure under scalar multiplication and $\lambda u + v \in W$ by closure under addition.

givenL1

2.1

Since $W$ was an arbitrary member of $\mathcal{W}$ , the vector $\lambda u + v$ lies in every member of $\mathcal{W}$ , that is $\lambda u + v \in U$ .

step 1.3

3.1

$U$ is a nonempty subset of $V$ satisfying the one-step test, hence a linear subspace of $V$ ; taking $\mathcal{W}$ to have two members gives the last sentence of the statement.

step 1.1step 1.2step 2.1L2∎

Remarks

The hypothesis that $\mathcal{W}$ is nonempty is load bearing. The intersection of the empty family of subsets of $V$ is not a subset of $V$ by any convention used here, and step 1.1 is where the hypothesis is spent. The same hypothesis appears for the same reason in The intersection of a nonempty family of subgroups of $G$ is a subgroup of $G$ .
This is what makes the span definable. The set of linear subspaces of $V$ containing a given subset $S$ is nonempty, since $V$ itself belongs to it, so its intersection is a linear subspace, and it is by construction the smallest linear subspace containing $S$ . That is Linear combination of a finite list, and the span $\operatorname{span}(S)$ as the smallest linear subspace containing $S$ , and the pattern is copied from The subgroup $\langle S \rangle$ generated by a subset, the cyclic subgroup $\langle g \rangle$ , and cyclic groups.
Unions behave quite differently. The union of two linear subspaces is almost never a linear subspace, and the companion examples page records the failure as a false statement.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 17 results over 13 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

Linear subspace (Wikipedia) (standard reference, not scraped)
S. Axler, Linear Algebra Done Right, 4th ed., Ch. 1 (standard reference, not scraped)

The intersection of a nonempty family of linear subspaces of VVV is a linear subspace of VVV