Salut,
Le message de Ben est effectivement un peu lacunaire, s'adressant plutôt à moi je suppose. Pour moi qui connait le probleme, tout va bien, mais effectivement, pour les autres, il faut plus voir ça comme des indications sur des idées à suivre que comme une solution à proprement parler. Du coup formaliser le tout reste un défi ouvert
L'idée est effectivement assez proche de l'extraction diagonale (bien qu'un peu différent dans ce cas précis).
Ce qui d'aprés moi se rapproche le plus de la solution est la preuve de Bolzano Weirstrass classique, i.e. de toute suite réelle bornée on peut extraire une sous suite convergente.
Rappel de la preuve (là encore, lacunaire): Soit
une suite bornée, disons dans [0,1]. On divise cet intervalle [0,1] en deux intervalles de longueur 1/2 et on choisit l'un des deux, qu'on appelle
, tel que l'ensemble
est infini. Puis on divise à son tour
en deux intervalles de longueur 1/4 et on choisit un des deux, qu'on appelle
, tel que
est infini. Continuant, on construit ainsi une suite
emboitée d'intervalles de plus en plus petits tel que
est infini pour tout k, puis finalement grâce à une extraction diagonale sur les
on construit une sous suite de
convergente.
Bon ben pour l'exercice, faut essentiellement adapter ça. Vu qu'on est dans un espace métrique compact, au lieu de diviser des intervalle en deux on va recouvrir des boules par des boules plus petites, et au vu de la restriction que l'on veut, plutôt que de regarder le cardinal des ensembles on va regarder la somme des inverses des éléments. Et aussi l'extraction diagonale à la fin n'est pas tout à fait diagonale...