Closed subspaces of Čech-complete spaces are Čech-complete

Given: The objects, hypotheses, and choice principles stated above.

A Tychonoff space $X$ is Čech-complete when there is a Hausdorff compactification $(K,i)$ of $X$ (def-compactification-of-a-tychonoff-space) for which $i[X]$ is a $G_{\delta }$ subset of $K$ (def-g-delta-and-f-sigma-in-a-topological-space). The definition asks for one compactification; thm-cech-completeness-is-independent-of-compactification proves the equivalent every-compactification form. (Čech-complete spaces as $G_{\delta }$ subspaces of Hausdorff compactifications).

Let $(X,\mathcal{T})$ be a topological space (def-topological-space), with subspaces as in def-subspace-topology-top and compactness as in def-compact-space. Then: 1. Closed in compact is compact. If $(X,\mathcal{T})$ is compact and $F\subseteq X$ is closed in $X$, then $F$ is a compact subset of $X$. 2. Finite unions. If $n\in \mathbb{N}$ and $K_0,\dots ,K_n$ are compact subsets of $X$, then $K_0\cup \cdots \cup K_n$ is a compact subset of $X$. The union of the empty list is $\mathrm{\varnothing }$, which is a compact subset of every space. Claim 1 needs $X$ to be compact and claim 2 does not; no hypothesis of any kind is placed on $X$ in claim 2. No choice principle is used: claim 1 selects nothing, taking a least index where a selection would be natural, and claim 2 makes finitely many selections through lem-finite-choice, a theorem of ZF. (A closed subspace of a compact space is compact, and a finite union of compact subspaces is compact).

Let $(X,\mathcal{T})$ be a Hausdorff topological space (def-hausdorff-space, def-topological-space), with compact subsets as in def-compact-space. Then: 1. A point and a disjoint compact set are separated. If $K\subseteq X$ is compact and $x\in X\setminus K$, there are $U,V\in \mathcal{T}$ with $x\in U,K\subseteq V,U\cap V=\mathrm{\varnothing }\mathrm{.}$ 2. Two disjoint compact sets are separated. If $K,L\subseteq X$ are compact and $K\cap L=\mathrm{\varnothing }$, there are $U,V\in \mathcal{T}$ with $L\subseteq U,K\subseteq V,U\cap V=\mathrm{\varnothing }\mathrm{.}$ 3. Compact implies closed. Every compact subset of $X$ is closed in $X$. 4. In a compact Hausdorff space the two classes coincide. If in addition $(X,\mathcal{T})$ is compact, then a subset of $X$ is compact if and only if it is closed. The proof is written choice-free, and that is not a stylistic preference. The textbook argument says "for each $y\in K$ choose disjoint open $U_y,V_y$", which is a selection over an arbitrary index set and therefore an appeal to the full Axiom of Choice. What is done below instead is to take the family of all open $V$ that admit some open $U\ni x$ disjoint from them — a family cut out by a formula, with nothing selected — extract a finite subcover from it, and only then make finitely many selections, which lem-finite-choice supplies as a theorem of ZF. (In a Hausdorff space a point and a disjoint compact set, and two disjoint compact sets, have disjoint open neighbourhoods; hence every compact subset is closed, and in a compact Hausdorff space the compact subsets are exactly the closed ones).