IsarMathLib

A library of formalized mathematics for Isabelle/ZF theorem proving environment

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 \{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 \{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 \{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 \{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 \{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 \)
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\}) \)

shows \( (\bigcup N) \text{ is closed in } T \)
lemma (in topology0) cl_contains_set:

assumes \( A \subseteq \bigcup T \)

shows \( A \subseteq cl(A) \)
lemma (in topology0) open_neigh_open:

assumes \( \forall x\in V.\ \exists U\in T.\ (x\in U \wedge U\subseteq V) \)

shows \( V\in T \)
31
15
6
6