# Formalized Mathematics

Just another WordPress.com weblog

## 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.

See also TiddlyWiki rendering of this post.
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 0, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 73, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "github"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "english_confidence": 0.9234380722045898, "perplexity_flag": "head"}