Caractérisation des bases par le cardinal : énoncé (MPSI)

Une famille libre $\mathcal{L}$ a au plus $n$ vecteurs par le lemme fondamental. Si elle en a $n$, on la complète en une base (théorème de la base incomplète) ; cette base a $n$ vecteurs, donc on n'a rien ajouté : $\mathcal{L}$ est une base.

Si $\mathcal{G}$ est génératrice, on peut supposer $\mathcal{G}$ finie (sinon elle a plus de $n$ vecteurs) ; on en extrait une base, qui a $n$ vecteurs, donc $\mathcal{G}$ a au moins $n$ vecteurs. Si elle en a exactement $n$, la base extraite est $\mathcal{G}$ elle-même.