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

About these ads

Tags: proofs topology