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 (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 is open. To do this, choose an arbitrary point . Since is , for every point we can find an open set such that . Obviously covers , so select a finite subcollection that covers , and so on. I had never realized that such reasoning requires the Axiom of Choice. Namely, suppose we have a lemma that states “In spaces, if , then there is an open set such that and ” (like our lemma *T2_cl_open_sep* below). This only states that the set of such open sets is not empty. To get the collection in this proof we have to select one such set among many for every and this is where we use the Axiom of Choice. Probably in 99/100 cases when an informal calculus proof states something like 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 space compact sets are closed.

**Compact sets are closed – no need for AC**

In this section we show that in a topological space compact sets are closed.

First we prove a lemma that in a space two points can be separated by the closure of an open set.

```
```**lemma** (in topology0) T2_cl_open_sep:
**assumes** A1: **and** A2:
**shows**
**proof** -
**from** A1 A2 **have**
**using** isT2_def
**then** **obtain** U V **where**
**then** **have** **using** open_disj_cl_disj
**thus**
**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 and *Fin(A)* is the set of finite subsets of .

```
```**theorem** (in topology0) in_t2_compact_is_cl:
**assumes** A1: **and** A2:
**shows**
**proof** -
**let** X =
**have**
**proof** -
** {** **fix** y **assume** A3:
**have**
**proof** -
**let** B =
**have** I:
**using** Fin.dom_subset
**from** A2 A3 **have**
**using** IsCompact_def
**with** A1 **have**
**using** T2_cl_open_sep
**hence**
**with** A2 I **have** **using** IsCompact_def
**then** **obtain** N **where** D1:
**with** I **have**
**hence** II:
**let** M =
**let** C =
**from** topSpaceAssum **have**
**using** IsATopology_def cl_is_closed IsClosed_def
**hence**
**moreover** **from** D1 **have**
**ultimately** **have** **by** (**rule** fin_image_fin)
**then** **have** **using** Top_3_L6 IsClosed_def
**moreover** **from** A3 II **have**
**moreover** **have**
**proof** -
**from** II **have** **using** cl_contains_set
**with** D1 **show**
**qed**
**ultimately** **have**
**thus**
**qed**
** }** **thus**
**qed**
**with** A2 **show**
**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.

Tags: proofs topology

## Leave a Reply