|
On suppose donc que toute famille NFC d'<u>ouverts de ''A''</u> est NC, et il s'agit de montrer qu'il en est de même pour les familles d'<u>ouverts quelconques</u>.
Soit ''F'' une famille NFC d'ouverts. Soit ''E'' l'ensemble des familles NFC d'ouverts dont ''F'' est une sous-famille. Alors, (''E'', ⊂) est [[w:Ensemble inductif|inductif]], c'est-à-dire que tout sous-ensemble ''E’C'' de ''E'' sur lequel l'ordre ⊂ est total admet un majorant (un élément de ''E'' dans lequel tous les éléments de ''E’C'' sont inclus) : il suffit de prendre la réunion des éléments de ''E’C'' (elle est bien NFC, car toute sous-famille finie de cette réunion est une sous-famille de l'un des éléments de ''E’C''). D'après le [[w:Lemme de Zorn|lemme de Zorn]], (''E'', ⊂) admet donc un [[w:Élément maximal|élément maximal]] ''F’G''. Nous allons montrer que ''F’G'' est NC (''a fortiori'', ''F'' sera NC).
Remarquons que par maximalité de ''F’G'', un ouvert ''U'' n'appartient pas à ''F’G'' (si et) seulement si ''X'' est recouvert par ''U'' et une réunion finie d'ouverts de ''F’G''. Par conséquent, l'ensemble des ouverts n'appartenant pas à ''F’G'' est stable par intersections finies et par « sur-ouverts » (ouverts contenant un élémentouvert de cet ensembledonné).
''A''∩''F’G'' est NFC (car ''G'' ∈ ''E'') donc est NC (par hypothèse sur ''A'') :
:<math>X\not\subset\cup_{V\in A\cap F'G}UV</math>.
Pour conclure que ''F’G'' est NC, il ne reste plus qu'à vérifier que
:<math>\cup_{U\in F'G}U\subset\cup_{V\in A\cap F'G}V</math>.
Soient <math>U\in F'G</math> et <math>x\in U</math>. Comme ''A'' est une prébase, il existe <math>V_1,\dots,V_n\in A</math> tels que <math>x\in V_1\cap\dots\cap V_n\subset U</math>. D'après la remarque précédente, l'un des <math>V_i</math> appartient alors à ''F’G'', ce qui achève la preuve.
}}
{{Démonstration déroulante|titre=Preuve du théorème de Tychonoff|contenu=
| 