Let $V$ be a vector space. If we assume $\AC$, $V$ has a basis by BAS > Proposition 3, and by BAS > Proposition 5, all bases of $V$ have the same length. This length is called the dimension of $V$, denoted by $\dim V$.
$V$ is finite-dimensional if $\dim V$ is finite; infinite-dimensional if $\dim V$ is infinite.
Let $V$ be a vector space. For any subspace $W \subseteq V$:
- \[\dim W \leq \dim V.\]
- \[\dim W = \dim V \enspace\rimp\enspace W = V.\]