IsarMathLib

Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

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 \( T \text{ is }T_2 \) and \( x \in \bigcup T \), \( y \in \bigcup T \), \( x\neq y \)

shows \( \exists U\in T.\ (x\in U \wedge y \notin cl(U)) \)proof

from assms 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 cl(U) \cap V = 0 \) using disj_open_cl_disj

thus \( \exists U\in T.\ (x\in U \wedge y \notin 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 \( \text{FinPow}(A) \) denotes the set of finite subsets of \(A\) in IsarMathLib.

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 \( 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 cl(V)\} \)

have I: \( B \in Pow(T) \), \( \text{FinPow}(B) \subseteq Pow(B) \) using FinPow_def

from \( K \text{ is compact in } T \), \( y \in X \), \( y\notin K \) have \( \forall x\in K.\ x \in X \wedge y \in X \wedge x\neq y \) using IsCompact_def

with \( T \text{ is }T_2 \) have \( \forall x\in K.\ \{V\in T.\ x\in V \wedge y \notin cl(V)\} \neq 0 \) using T2_cl_open_sep

hence \( K \subseteq \bigcup B \)

with \( K \text{ is compact in } T \), I have \( \exists N \in \text{FinPow}(B).\ K \subseteq \bigcup N \) using IsCompact_def

then obtain \( N \) where \( N \in \text{FinPow}(B) \), \( K \subseteq \bigcup N \)

with I have \( N \subseteq B \)

hence \( \forall V\in N.\ V\in B \)

let \( M = \{cl(V).\ V\in N\} \)

let \( C = \{D \in Pow(X).\ D \text{ is closed in } T\} \)

from \( N \in \text{FinPow}(B) \) have \( \forall V\in B.\ cl(V) \in C \), \( N \in \text{FinPow}(B) \) using cl_is_closed, IsClosed_def

then have \( M \in \text{FinPow}(C) \) by (rule fin_image_fin )

then have \( X - \bigcup M \in T \) using fin_union_cl_is_cl, IsClosed_def

moreover

from \( y \in X \), \( y\notin K \), \( \forall V\in N.\ V\in B \) have \( y \in X - \bigcup M \)

moreover

have \( X - \bigcup M \subseteq X - K \)proof

from \( \forall V\in N.\ V\in B \) have \( \bigcup N \subseteq \bigcup M \) using cl_contains_set

with \( K \subseteq \bigcup N \) 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

Definition of isT2: \( T \text{ is }T_2 \equiv \forall x y.\ ((x \in \bigcup T \wedge y \in \bigcup T \wedge x\neq y) \longrightarrow \) \( (\exists U\in T.\ \exists V\in T.\ x\in U \wedge y\in V \wedge U\cap V=0)) \)

lemma (in topology0) disj_open_cl_disj:

assumes \( A \subseteq \bigcup T \), \( V\in T \) and \( A\cap V = 0 \)

shows \( cl(A) \cap V = 0 \)

Definition of FinPow: \( \text{FinPow}(X) \equiv \{A \in Pow(X).\ Finite(A)\} \)

Definition of IsCompact: \( K \text{ is compact in } T \equiv (K \subseteq \bigcup T \wedge \) \( (\forall M\in Pow(T).\ K \subseteq \bigcup M \longrightarrow (\exists N \in \text{FinPow}(M).\ K \subseteq \bigcup N))) \)

lemma (in topology0) T2_cl_open_sep:

assumes \( T \text{ is }T_2 \) and \( x \in \bigcup T \), \( y \in \bigcup T \), \( x\neq y \)

shows \( \exists U\in T.\ (x\in U \wedge y \notin cl(U)) \)

lemma (in topology0) cl_is_closed:

assumes \( A \subseteq \bigcup T \)

shows \( cl(A) \text{ is closed in } T \) and \( \bigcup T - cl(A) \in T \)

Definition of IsClosed: \( D \text{ is closed in } T \equiv (D \subseteq \bigcup T \wedge \bigcup T - D \in T) \)

lemma fin_image_fin:

assumes \( \forall V\in B.\ K(V)\in C \) and \( N \in \text{FinPow}(B) \)

shows \( \{K(V).\ V\in N\} \in \text{FinPow}(C) \)

lemma (in topology0) fin_union_cl_is_cl:

assumes \( N \in \text{FinPow}(\{D\in Pow(\bigcup T).\ D \text{ is closed in } T\}) \)