Alphabeta Math
DefinitionDefinition: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)judge 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.

Linear combination of a finite list, and the span span(S)\operatorname{span}(S) as the smallest linear subspace containing SS

Definition

Let VV be a vector space over a field FF (Vector space over a field).

Finite sums of vectors

By axiom (V1) the triple (V,+,0V)(V, +, 0_V) is an abelian group (Group and abelian group), hence in particular a commutative monoid (Semigroup and monoid). So the finite products of The product g0g1gn1g_0 g_1 \cdots g_{n-1} of a finite list in a monoid, by recursion, with the empty product (n=0n = 0) equal to the identity are available in it, and we write them additively: for nNn \in \mathbb{N} and a finite list u:nVu : n \to V, that is a function on the von Neumann natural n={0,,n1}n = \{0, \dots, n-1\} (The natural numbers N\mathbb{N} (von Neumann), On N\mathbb{N} the order is membership: m<n    mnm < n \iff m \in n),

i<nui  :=  i<nuicomputed in (V,+,0V),\sum_{i<n} u_i \;:=\; \prod_{i<n} u_i \quad \text{computed in } (V,+,0_V),

so that i<0ui=0V\sum_{i<0} u_i = 0_V and i<σ(n)ui=(i<nui)+un\sum_{i<\sigma(n)} u_i = \bigl(\sum_{i<n} u_i\bigr) + u_n, and the value depends only on u0,,un1u_0, \dots, u_{n-1}.

Linear combinations

A linear combination in VV is a vector of the form

i<nλivi\sum_{i<n} \lambda_i v_i

where nNn \in \mathbb{N}, λ:nF\lambda : n \to F is a finite list of scalars and v:nVv : n \to V is a finite list of vectors; the sum is the finite sum just described, of the list iλivii \mapsto \lambda_i v_i. For SVS \subseteq V, a vector wVw \in V is a linear combination of elements of SS when there are nNn \in \mathbb{N}, λ:nF\lambda : n \to F and v:nSv : n \to S with w=i<nλiviw = \sum_{i<n} \lambda_i v_i.

The empty case is a real case. N\mathbb{N} contains 00 (The natural numbers N\mathbb{N} (von Neumann)), and at n=0n = 0 the sum is the empty sum, which is 0V0_V. So 0V0_V is a linear combination of elements of every subset of VV, including S=S = \varnothing. The lists are indexed from 00, so a linear combination of length nn is λ0v0++λn1vn1\lambda_0 v_0 + \dots + \lambda_{n-1}v_{n-1}; no statement here is restricted to n1n \ge 1.

The span

Let SVS \subseteq V. The set of linear subspaces of VV containing SS is nonempty, since VV itself is one, so its intersection is a linear subspace of VV by The intersection of a nonempty family of linear subspaces of VV is a linear subspace of VV. That intersection is the span of SS,

span(S)  :=  {W  :  W is a linear subspace of V and SW}.\operatorname{span}(S) \;:=\; \bigcap \{\, W \;:\; W \text{ is a linear subspace of } V \text{ and } S \subseteq W \,\} .

It contains SS, being an intersection of sets each of which contains SS, and it is contained in every linear subspace of VV that contains SS. So it is the smallest linear subspace of VV containing SS, and those two properties determine it uniquely: if WW and WW' both contain SS and are each contained in every linear subspace containing SS, then each is contained in the other. This is what licenses the definite article.

A subset SVS \subseteq V spans VV, or is a spanning set of VV, when span(S)=V\operatorname{span}(S) = V.

Remarks

Depends on

Used by

…and 8 more results.

Dependency tree · next 3 levels

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