IsarMathLib

One of the facts demonstrated in every class on General Topology is that in a $T_2$ (Hausdorff) topological space compact sets are closed. Formalizing the proof of this fact gave me an interesting insight into the role of the Axiom of Choice (AC) in many informal proofs.

A typical informal proof of this fact goes like this: we want to show that the complement of $K$ is open. To do this, choose an arbitrary point $y\in K^c$. Since $X$ is $T_2$, for every point $x\in K$ we can find an open set $U_x$ such that $y\notin \overline{U_x}$. Obviously $\{U_x{\}}_{x\in K}$ covers $K$, so select a finite subcollection that covers $K$, and so on. I had never realized that such reasoning requires the Axiom of Choice. Namely, suppose we have a lemma that states "In $T_2$ spaces, if $x\ne y$, then there is an open set $U$ such that $x\in U$ and $y\notin \bar{U}$" (like our lemma T2_cl_open_sep below). This only states that the set of such open sets $U$ is not empty. To get the collection $\{U_x{\}}_{x\in K}$ in this proof we have to select one such set among many for every $x\in K$ and this is where we use the Axiom of Choice. Probably in 99/100 cases when an informal calculus proof states something like $\mathrm{\forall }\epsilon \mathrm{\exists }{\delta }_{\epsilon }\cdots$ the proof uses AC. Most of the time the use of AC in such proofs can be avoided. This is also the case for the fact that in a $T_2$ space compact sets are closed.

In this section we show that in a $T_2$ topological space compact sets are closed.

First we prove a lemma that in a $T_2$ space two points can be separated by the closure of an open set.

AC-free proof that in a Hausdorff space compact sets are closed. To understand the notation recall that in Isabelle/ZF $Pow(A)$ is the powerset (the set of subsets) of $A$ and $\text{FinPow}(A)$ denotes the set of finite subsets of $A$ in IsarMathLib.