Inverser des quantificateurs grace au lemme de Baire

Un situation qui pue le Baire est la suivante : on veut passer d'une propriete du type

a la propriete ou est une partie denombrable (on a rendu le independant du point ).

Souvent, c'est le meme schema de preuve qui fait marcher le truc, voici une esquisse simple :

1. On pose
2. Avec un peu de chance (ou en forcant le destin) est un espace metrique complet et y est ferme (la propriete met en jeu des fonctions continues par exemple) donc on peut appliquer le lemme de Baire : l'un des est d'interieur non vide (on cree une breche).
3. Reste a etaler le truc, souvent au moyen d'homogeneite, par exemple
   • lorsque les sont des sous espaces vectoriels du Banach :
     • NilpotentsBanach
     • CaracterisationDiracs
     • BanachSteinhaus
     • ...
   • grace a un argument de connexite, zeros isoles, techniques de maillage :
     • CaracterisationPolynomes

Un tel schema de preuve est parfois appele bairette ; c'est un peu comme une zornette, mais pour le lemme de Baire
to top