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.

$\sum_{i<n} U_i = \operatorname{span}\bigl(\bigcup_{i<n} U_i\bigr)$ , so the sum is the smallest linear subspace containing every $U_i$

Statement

Let $V$ be a vector space over a field $F$ (Vector space over a field), let $n \in \mathbb{N}$ , and let $U$ be a finite family of linear subspaces $U_i$ of $V$ indexed by $i < n$ (The sum $U + W$ of two linear subspaces and the sum $\sum_{i<n} U_i$ of a finite family). Write

$\bigcup_{i<n} U_i \;=\; \{\, x \in V \;:\; x \in U_i \text{ for some } i < n \,\}.$

Then

$\sum_{i<n} U_i \;=\; \operatorname{span}\Bigl(\bigcup_{i<n} U_i\Bigr),$

so $\sum_{i<n} U_i$ is the smallest linear subspace of $V$ containing $U_i$ for every $i < n$ : it contains each $U_i$ , and it is contained in every linear subspace of $V$ that contains each $U_i$ .

Facts & Assumptions

Given: A field $F$ , a vector space $V$ over $F$ , a natural number $n$ , and a family of linear subspaces $U_i$ of $V$ indexed by $i < n$ .

[L1]

$\sum_{i<n} U_i$ is a linear subspace of $V$ whose elements are exactly the vectors $\sum_{i<n} u_i$ with $u_i \in U_i$ for every $i < n$ ; and a list vanishing off a single index $j < n$ sums to its value at $j$ (The sum $U + W$ of two linear subspaces and the sum $\sum_{i<n} U_i$ of a finite family).

[L2]

For $T \subseteq V$ , the span $\operatorname{span}(T)$ is a linear subspace of $V$ containing $T$ and contained in every linear subspace of $V$ containing $T$ (Linear combination of a finite list, and the span $\operatorname{span}(S)$ as the smallest linear subspace containing $S$ ).

[L3]

A linear subspace contains $0_V$ by (W1) and is closed under $+$ by (W2) (Linear subspace of a vector space).

[L4]

Finite sums in $(V,+,0_V)$ : $\sum_{i<0} u_i = 0_V$ and $\sum_{i<\sigma(m)} u_i = \bigl(\sum_{i<m} u_i\bigr) + u_m$ (The product $g_0 g_1 \cdots g_{n-1}$ of a finite list in a monoid, by recursion, with the empty product ( $n = 0$ ) equal to the identity, Linear combination of a finite list, and the span $\operatorname{span}(S)$ as the smallest linear subspace containing $S$ ).

[L5]

Induction on $\mathbb{N}$ , whose elements are the von Neumann naturals with $m = \{\, k : k < m \,\}$ (The principle of mathematical induction, The natural numbers $\mathbb{N}$ (von Neumann), On $\mathbb{N}$ the order is membership: $m < n \iff m \in n$ ).

Proof

technique · direct

1.1

Each $U_j$ with $j < n$ is contained in $\sum_{i<n} U_i$ : given $x \in U_j$ , let $u : n \to V$ be the list with $u_j = x$ and $u_i = 0_V$ for $i \ne j$ ; then $u_i \in U_i$ for every $i < n$ , since each $U_i$ contains $0_V$ , and this list sums to $x$ .

L1L3

1.2

A linear subspace $W$ of $V$ is closed under finite sums: for every $m \in \mathbb{N}$ and every list $u : m \to W$ , the vector $\sum_{i<m} u_i$ lies in $W$ . By induction on $m$ : at $m = 0$ the sum is $0_V \in W$ by (W1), and if it holds at $m$ then $\sum_{i<\sigma(m)} u_i = \bigl(\sum_{i<m} u_i\bigr) + u_m$ lies in $W$ by the inductive hypothesis and (W2).

L3L4L5

2.1

$\bigcup_{i<n} U_i \subseteq \sum_{i<n} U_i$ by step 1.1, and $\sum_{i<n} U_i$ is a linear subspace of $V$ , so the span of the union is contained in it: $\operatorname{span}\bigl(\bigcup_{i<n} U_i\bigr) \subseteq \sum_{i<n} U_i$ .

step 1.1L1L2

2.2

Conversely, $\operatorname{span}\bigl(\bigcup_{i<n} U_i\bigr)$ is a linear subspace of $V$ containing the union, hence containing each $U_i$ ; so any list $u : n \to V$ with $u_i \in U_i$ for every $i < n$ takes its values in it, and step 1.2 gives $\sum_{i<n} u_i \in \operatorname{span}\bigl(\bigcup_{i<n} U_i\bigr)$ . As these vectors are exactly the elements of $\sum_{i<n} U_i$ , that yields $\sum_{i<n} U_i \subseteq \operatorname{span}\bigl(\bigcup_{i<n} U_i\bigr)$ .

step 1.2L1L2

3.1

The two inclusions give $\sum_{i<n} U_i = \operatorname{span}\bigl(\bigcup_{i<n} U_i\bigr)$ .

step 2.1step 2.2

4.1

A linear subspace of $V$ contains $\bigcup_{i<n} U_i$ exactly when it contains $U_i$ for every $i < n$ , so the span of the union is the smallest linear subspace containing every $U_i$ ; by step 3.1 the sum is that subspace.

step 3.1L2∎

Remarks

The empty family is consistent with the statement. At $n = 0$ the union is $\varnothing$ and the sum is $\{0_V\}$ (The sum $U + W$ of two linear subspaces and the sum $\sum_{i<n} U_i$ of a finite family), while $\operatorname{span}(\varnothing) = \{0_V\}$ ( $\operatorname{span}(S)$ is exactly the set of linear combinations of finite lists of elements of $S$ , and $\operatorname{span}(\varnothing) = \{0_V\}$ ), so both sides agree. This is the case that would be lost if $\mathbb{N}$ started at $1$ .
What the identification buys. The left-hand side is concrete, a set of vectors one can produce; the right-hand side is a universal property, "smallest linear subspace containing all the $U_i$ ". Having both means the sum can be computed by exhibiting decompositions and bounded by minimality, which is how the examples on the companion page proceed.
This is the linear analogue of a familiar fact about subgroups. The subgroup generated by a union of subgroups is the smallest subgroup containing them all (The subgroup $\langle S \rangle$ generated by a subset, the cyclic subgroup $\langle g \rangle$ , and cyclic groups); here the sum plays that role, and no separate "generated by" notation is needed for linear subspaces because $\operatorname{span}(S)$ is exactly the set of linear combinations of finite lists of elements of $S$ , and $\operatorname{span}(\varnothing) = \{0_V\}$ already describes the span from inside.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 51 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

Linear subspace (Wikipedia) (standard reference, not scraped)
Linear span (Wikipedia) (standard reference, not scraped)
S. Axler, Linear Algebra Done Right, 4th ed. (free PDF, CC BY-NC) (standard reference, not scraped)

∑i<nUi=span⁡(⋃i<nUi)\sum_{i<n} U_i = \operatorname{span}\bigl(\bigcup_{i<n} U_i\bigr)∑i<n​Ui​=span(⋃i<n​Ui​), so the sum is the smallest linear subspace containing every UiU_iUi​