DIM#DEF. Dimension. $\limp\AC$
Let $V$ be a vector space. By BS#PROP-EX, $V$ has a basis. By BS#PROP-L, all bases of $V$ have the same cardinality. This cardinality is called the dimension of $V$, written as $\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$.