# 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