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.

Advertisements

Tags:

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s


%d bloggers like this: