Le produit de deux compacts est compact

$K \times L$ est séparé : si $(x,y) \neq (x',y')$, les points diffèrent par une coordonnée, disons $x \neq x'$, et des ouverts disjoints $U \ni x$, $U' \ni x'$ donnent les ouverts disjoints $U \times L$ et $U' \times L$.

Soit $\mathcal C$ un recouvrement ouvert de $K \times L$, et $\mathcal B$ l'ensemble des cylindres $U \times V$ inclus dans un élément de $\mathcal C$. Ils recouvrent $K \times L$, et il suffit d'en extraire un recouvrement fini : la collecte finie (Ensembles finis, sans les entiers, (vi)) en tire une partie finie de $\mathcal C$ telle que chaque élément de ce recouvrement soit inclus dans l'un des siens, et qui recouvre donc $K \times L$.

Lemme du tube. Pour $x \in K$, il existe un ouvert $U \ni x$ tel que $U \times L$ soit recouvert par une partie finie de $\mathcal B$.

En effet, les ouverts $V$ tels qu'il existe $U \times V \in \mathcal B$ avec $x \in U$ recouvrent $L$ ; on en extrait un recouvrement fini $\mathcal V$ de $L$. Appliquons la récurrence sur les parties de $\mathcal V$ (même nœud, (ii)) à la formule « il existe un ouvert $U \ni x$ et une partie finie $\mathcal B'$ de $\mathcal B$ tels que $U \times \bigcup \mathcal V' \subset \bigcup \mathcal B'$ », de variable $\mathcal V'$. Elle est vraie pour $\mathcal V' = \varnothing$, avec $U = K$ et $\mathcal B' = \varnothing$. Si elle l'est pour $\mathcal V'$, avec $U$ et $\mathcal B'$, et si $V \in \mathcal V$, soit $U_V \times V \in \mathcal B$ avec $x \in U_V$ : l'ouvert $U \cap U_V$ et la partie $\mathcal B' \cup \{U_V \times V\}$, finie par le point (iii) du même nœud, conviennent pour $\mathcal V' \cup \{V\}$. Elle est donc vraie pour $\mathcal V$, dont la réunion est $L$.

Soit $\mathcal W$ l'ensemble des ouverts $U$ de $K$ tels que $U \times L$ soit recouvert par une partie finie de $\mathcal B$. Par le lemme, $\mathcal W$ recouvre $K$ ; on en extrait un recouvrement fini $\mathcal W'$. La collecte finie, dans l'ensemble des parties finies de $\mathcal B$, fournit un ensemble fini $\mathfrak D$ de telles parties, tel que, pour chaque $U \in \mathcal W'$, la bande $U \times L$ soit recouverte par un élément de $\mathfrak D$. La réunion $\bigcup \mathfrak D$ est une partie finie de $\mathcal B$ (même nœud, (v)), qui recouvre $K \times L$.

Passons à une famille indexée par un ensemble fini $I$, et appliquons la récurrence sur les parties de $I$ (même nœud, (ii)) à la formule « $P_J = \prod_{i \in J} X_i$ est compact », de variable $J$. Pour $J = \varnothing$, le produit n'a qu'un élément, la famille vide, et un espace à un point est compact. Supposons $P_J$ compact, et soit $k \in I \setminus J$. L'application $g : P_J \times X_k \to P_{J \cup \{k\}}$ qui associe à $(u, y)$ la famille égale à $u$ sur $J$ et à $y$ en $k$ est surjective ; elle est continue par la propriété universelle du produit (Topologie produit), puisque ses composées avec les projections de $P_{J \cup \{k\}}$ sont la seconde projection, ou la composée de la première avec une projection de $P_J$. Le produit $P_J \times X_k$ est identifié, comme $K \times L$ plus haut, au produit de la famille de ses deux facteurs, dont les deux projections sont continues par la même proposition.

L'espace $P_J \times X_k$ est compact par ce qui précède. L'espace $P_{J \cup \{k\}}$ est séparé : deux familles distinctes diffèrent en un indice $i$, et les images réciproques par $p_i$ d'ouverts disjoints de $X_i$ les séparent. Enfin, si $\mathcal C$ est un recouvrement ouvert de $P_{J \cup \{k\}}$, les $g^{-1}(C)$, $C \in \mathcal C$, recouvrent $P_J \times X_k$ ; la collecte finie, appliquée à un recouvrement fini qu'on en extrait, fournit une partie finie $\mathcal C'$ de $\mathcal C$ dont les images réciproques recouvrent $P_J \times X_k$, et $\mathcal C'$ recouvre $P_{J \cup \{k\}}$, puisque $g$ est surjective. La formule est donc vraie pour $J \cup \{k\}$, puis pour $I$.