Compacts, fermés et images

(i) Soit $F$ fermé dans le compact $K$, séparé comme partie d'un séparé. Soit $\mathcal C$ un recouvrement de $F$ par des ouverts de $F$, et $\mathcal D$ l'ensemble des ouverts $O$ de $K$ tels que $O \cap F \in \mathcal C$.

Les éléments de $\mathcal D$ et l'ouvert $K \setminus F$ recouvrent $K$ ; on en extrait un recouvrement fini $\mathcal S$. Les traces sur $F$ des éléments de $\mathcal S \cap \mathcal D$ appartiennent à $\mathcal C$ et recouvrent $F$, que $K \setminus F$ ne rencontre pas. Elles forment un ensemble fini, image d'une partie de $\mathcal S$ (Ensembles finis, sans les entiers, (i) et (iv)), donc un sous-recouvrement fini de $\mathcal C$.

(ii) Soit $A$ compact dans le séparé $X$, et $x \notin A$. Soit $\mathcal U$ l'ensemble des ouverts $U$ de $X$ pour lesquels il existe un ouvert $V \ni x$ disjoint de $U$. Par séparation, leurs traces recouvrent $A$ ; on en extrait un recouvrement fini $\mathcal S$ de $A$. Chaque élément de $\mathcal S$ est la trace d'un élément de $\mathcal U$ : par la collecte finie (Ensembles finis, sans les entiers, (vi)), il existe une partie finie $\mathcal U'$ de $\mathcal U$ dont les traces comprennent les éléments de $\mathcal S$, de sorte que $A \subset \bigcup \mathcal U'$. Une seconde collecte, dans l'ensemble des ouverts qui contiennent $x$, fournit un ensemble fini $\mathcal V$ de tels ouverts, tel que chaque $U \in \mathcal U'$ soit disjoint d'un élément de $\mathcal V$.

L'ouvert $V$, égal à $\bigcap \mathcal V$ si $\mathcal V$ n'est pas vide (Espace topologique) et à $X$ sinon, contient $x$. Il ne rencontre aucun $U \in \mathcal U'$, puisqu'il est inclus dans un élément de $\mathcal V$ disjoint de $U$ ; il ne rencontre donc pas $A$. Ainsi $X \setminus A$ est voisinage de chacun de ses points : il est ouvert.

(iii) $f(K)$ est séparé comme partie de $Y$. Soit un recouvrement de $f(K)$ par des ouverts de $f(K)$, et $\mathcal W$ l'ensemble des ouverts $W$ de $Y$ dont la trace sur $f(K)$ appartient à ce recouvrement. Les $f^{-1}(W)$, pour $W \in \mathcal W$, recouvrent $K$ ; on en extrait un recouvrement fini $\mathcal S$. Par la collecte finie (Ensembles finis, sans les entiers, (vi)), il existe une partie finie $\mathcal W'$ de $\mathcal W$ telle que chaque élément de $\mathcal S$ soit de la forme $f^{-1}(W)$ avec $W \in \mathcal W'$. Les traces sur $f(K)$ des éléments de $\mathcal W'$, en nombre fini par le point (iv) du même nœud, recouvrent $f(K)$, puisque les $f^{-1}(W)$, $W \in \mathcal W'$, recouvrent $K$.