Espace vectoriel sans famille génératrice

Super intéressant, je vais m'intéresser sur cet axiome, je ne le connais pas du tout.
@GaBuZoMeu Je ne comprends pas ce que tu veux dire par fini. Si tu parles d'un ev de dimension finie, alors par définition il admet une famille génératrice et donc une base par le théorème de la base extraite.

En fait ce qui m'a amené à ce questionnement est la formulation que j'ai eu d'un corollaire du théorème de la base de extraite.
Enoncé : Soit E un espace vectoriel de dimension finie. Alors E possède une base.
Tel que formulé, il permet de prouver l'existence d'une base. Je me suis alors demandé si il était possible d'avoir un espace vectoriel ne possédant pas de famille génératrice.
La réponse semble évidemment être non mais je trouve la formulation du corollaire un petit peu bizarre.
En effet, comme tout espace vectoriel possède une famille génératrice, alors d'après le théorème de la base extraite, on peut forcément trouver une base de l'espace que génère cette famille.

Alors je suppose que peu importe le cas c'est à dire un espace vectoriel de dimension finie ou infinie, on peut trouver une famille génératrice ?

C'est clair à présent, comme ce sont des notions nouvelles j'étais un petit perdu, désolé ^^

1) Je suis partie de la façon suivante : Toute espace vectoriel possède au moins une famille génératrice, séparons 2 cas :
1er cas : Une famille génératrice de notre espace E a nombre finie de vecteurs, alors E est dimension finie par définition
2ème cas: Une famille génératrice de notre espace E a un nombre infinie de vecteurs. Comme cette famille est infinie, elle est liée. On peut donc exprimer un vecteur de cette famille comme combinaison linéaire des autres vecteurs de cette famille. En utilisant un lemme qui permet d'égaliser les deux Vect (celui qui contient ce vecteur qu'on a exprimé comme CL des autres et celui ne le contenant pas), on peut aboutir par décroissance à une famille libre (car la famille vide est libre dans le pire des cas). Je ne vois pas comment poursuivre à partir de là, c'est-à-dire pour montrer que cette famille est génératrice.

2) Si E est dimension finie, alors elle admet une famille génératrice finie. Si on note k le nombre de vecteurs de cette famille, on a dim(E) = k.
Par un lemme, on a donc que toute famille de k+1 vecteurs est liée. Donc pour tout n > k, la famille de E de n vecteurs est liée.

Merci christophe, je vais essayer de me dégager du temps pour dans un premier temps faire ton exercice sur une feuille et dans un second temps m'intéresser à l'axiome du choix.
Encore merci à tout le monde pour votre aide précieuse.