## Vector space basis

### Set

 context $V$…$\ \mathcal F$-vector space
 definiendum $B\in \mathrm{basis}(V)$
 context $B\subset V$
 $B'\subseteq B$ $B'$…finite range $n\equiv\left|B'\right|$
 $v_1,\dots,v_n\in B'$ $c_1,\dots c_n\in \mathcal F$ $x\in V$
 postulate $\sum_{k=1}^n c_k\cdot v_k=0\ \Rightarrow\ \forall j.\ c_j=0$

All finite subsets of the base are linearly independed. It's maybe more clear when written in the contrapositive: “$\exists j.\ c_j\ne 0\ \Rightarrow\ \sum_{k=1}^n c_k\cdot v_k\ne 0$.”

 postulate $\exists c_1,\dots,c_n.\ (x=\sum_{k=1}^n c_k\cdot v_k)$

For each basis $B$, every vector $x\in V$ has representation as linear combination.

### Discussion

We call the vector space finite if it has a finite basis.

The difficulty in defining the basis of a general vector space above, and the reason why one must consider finite subsets $B'$ of the base $B$, is that an infinite sum would require more structure than just what a general vector space provides (e.g. a metric w.r.t. which the series converges).

The zero vector space has an empty base. Its vector space dimension is zero.

### Reference

Wikipedia: Vector space