## Compact sets and the Axiom of Choice

The first iteration of the tool for extracting blog-postable view from Isabelle/ZF source is ready. The post below is the result of processing the Topology_ZF_1b.thy theory file, to be included on the next release of IsarMathLib. The tool just does a bunch of context-sensitive text substitutions. The next iteration will hopefully do something closer to real parsing of the Isar source.

theory Topology_ZF_1b imports Topology_ZF_1

begin

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\neq y$, then there is an open set $U$ such that $x\in U$ and $y\notin \overline{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 $\forall \varepsilon \exists \delta_\varepsilon \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.

Compact sets are closed – no need for AC

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.

lemma (in topology0) T2_cl_open_sep:
assumes A1: $T \text{ is}\ T_2 \$  and A2: $x \in \bigcup T$  $y \in \bigcup T$   $x\neq y$
shows $\exists U\in T.\ (x\in U \wedge y \notin \text{cl}(U))$
proof -
from A1 A2 have $\exists U\in T.\ \exists V\in T.\ x\in U \wedge y\in V \wedge U\cap V=0$
using isT2_def
then obtain U V where $U\in T$  $V\in T$  $x\in U$  $y\in V$  $U\cap V=0$
then have $U\in T \wedge x\in U \wedge y\in V \wedge \text{cl}(U) \cap V = 0$ using open_disj_cl_disj
thus $\exists U\in T.\ (x\in U \wedge y \notin \text{cl}(U))$
qed

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 Fin(A) is the set of finite subsets of $A$.

theorem (in topology0) in_t2_compact_is_cl:
assumes A1: $T \text{ is}\ T_2 \$ and A2: $K \text{ is compact in}\ T$
shows $K \text{ is closed in}\ T$
proof -
let X = $\bigcup T$
have $\forall y \in X - K.\ \exists U\in T.\ y\in U \wedge U \subseteq X - K$
proof -
{ fix y assume A3: $y \in X$  $y\notin K$
have $\exists U\in T.\ y\in U \wedge U \subseteq X - K$
proof -
let B = $\bigcup x\in K.\ \{V\in T.\ x\in V \wedge y \notin \text{cl}(V)\}$
have I: $B \in \text{Pow}(T)$  $\text{Fin}(B) \subseteq \text{Pow}(B)$
using Fin.dom_subset
from A2 A3 have $\forall x\in K.\ x \in X \wedge y \in X \wedge x\neq y$
using IsCompact_def
with A1 have $\forall x\in K.\ \{V\in T.\ x\in V \wedge y \notin \text{cl}(V)\} \neq 0$
using T2_cl_open_sep
hence $K \subseteq \bigcup B$
with A2 I have $\exists N \in \text{Fin}(B).\ K \subseteq \bigcup N$ using IsCompact_def
then obtain N where D1: $N \in \text{Fin}(B)$  $K \subseteq \bigcup N$
with I have $N \subseteq B$
hence II: $\forall V\in N.\ V\in B$
let M = $\{\text{cl}(V).\ V\in N\}$
let C = $\{D \in \text{Pow}(X).\ D \text{ is closed in}\ T\}$
from topSpaceAssum have
$\forall V\in B.\ (\text{cl}(V) \text{ is closed in}\ T)$
$\forall V\in B.\ (\text{cl}(V) \in \text{Pow}(X))$
using IsATopology_def cl_is_closed IsClosed_def
hence $\forall V\in B.\ \text{cl}(V) \in C$
moreover from D1 have $N \in \text{Fin}(B)$
ultimately have $M \in \text{Fin}(C)$ by (rule fin_image_fin)
then have $X - \bigcup M \in T$ using Top_3_L6 IsClosed_def
moreover from A3 II have $y \in X - \bigcup M$
moreover have $X - \bigcup M \subseteq X - K$
proof -
from II have $\bigcup N \subseteq \bigcup M$ using cl_contains_set
with D1 show $X - \bigcup M \subseteq X - K$
qed
ultimately have $\exists U.\ U\in T \wedge y \in U \wedge U \subseteq X - K$
thus $\exists U\in T.\ y\in U \wedge U \subseteq X - K$
qed
} thus $\forall y \in X - K.\ \exists U\in T.\ y\in U \wedge U \subseteq X - K$
qed
with A2 show $K \text{ is closed in}\ T$
using open_neigh_open IsCompact_def IsClosed_def
qed

end

This blog post has been generated from IsarMathLib’s Topology_ZF_1b.thy theory file, see the relevant pages of the IsarMathLib proof document.