src/HOL/Topological_Spaces.thy

--- a/src/HOL/Topological_Spaces.thy	Tue Dec 17 22:34:26 2013 +0100
+++ b/src/HOL/Topological_Spaces.thy	Wed Dec 18 11:53:40 2013 +0100
@@ -1906,6 +1906,47 @@
     by (intro exI[of _ "D - {-t}"]) auto
 qed
 
+lemma inj_setminus: "inj_on uminus (A::'a set set)"
+  by (auto simp: inj_on_def)
+
+lemma compact_fip:
+  "compact U \<longleftrightarrow>
+    (\<forall>A. (\<forall>a\<in>A. closed a) \<longrightarrow> (\<forall>B \<subseteq> A. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {}) \<longrightarrow> U \<inter> \<Inter>A \<noteq> {})"
+  (is "_ \<longleftrightarrow> ?R")
+proof (safe intro!: compact_eq_heine_borel[THEN iffD2])
+  fix A
+  assume "compact U"
+    and A: "\<forall>a\<in>A. closed a" "U \<inter> \<Inter>A = {}"
+    and fi: "\<forall>B \<subseteq> A. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {}"
+  from A have "(\<forall>a\<in>uminus`A. open a) \<and> U \<subseteq> \<Union>(uminus`A)"
+    by auto
+  with `compact U` obtain B where "B \<subseteq> A" "finite (uminus`B)" "U \<subseteq> \<Union>(uminus`B)"
+    unfolding compact_eq_heine_borel by (metis subset_image_iff)
+  with fi[THEN spec, of B] show False
+    by (auto dest: finite_imageD intro: inj_setminus)
+next
+  fix A
+  assume ?R
+  assume "\<forall>a\<in>A. open a" "U \<subseteq> \<Union>A"
+  then have "U \<inter> \<Inter>(uminus`A) = {}" "\<forall>a\<in>uminus`A. closed a"
+    by auto
+  with `?R` obtain B where "B \<subseteq> A" "finite (uminus`B)" "U \<inter> \<Inter>(uminus`B) = {}"
+    by (metis subset_image_iff)
+  then show "\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T"
+    by  (auto intro!: exI[of _ B] inj_setminus dest: finite_imageD)
+qed
+
+lemma compact_imp_fip:
+  "compact s \<Longrightarrow> \<forall>t \<in> f. closed t \<Longrightarrow> \<forall>f'. finite f' \<and> f' \<subseteq> f \<longrightarrow> (s \<inter> (\<Inter> f') \<noteq> {}) \<Longrightarrow>
+    s \<inter> (\<Inter> f) \<noteq> {}"
+  unfolding compact_fip by auto
+
+lemma compact_imp_fip_image:
+  "compact s \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> closed (f i)) \<Longrightarrow> (\<And>I'. finite I' \<Longrightarrow> I' \<subseteq> I \<Longrightarrow> (s \<inter> (\<Inter>i\<in>I'. f i) \<noteq> {})) \<Longrightarrow>
+    s \<inter> (\<Inter>i\<in>I. f i) \<noteq> {}"
+  using finite_subset_image[of _ f I] compact_imp_fip[of s "f`I"] unfolding ball_simps[symmetric] INF_def
+  by (metis image_iff)
+
 end
 
 lemma (in t2_space) compact_imp_closed: