src/HOL/Topological_Spaces.thy
 changeset 54797 be020ec8560c parent 54258 adfc759263ab child 55415 05f5fdb8d093
```     1.1 --- a/src/HOL/Topological_Spaces.thy	Tue Dec 17 22:34:26 2013 +0100
1.2 +++ b/src/HOL/Topological_Spaces.thy	Wed Dec 18 11:53:40 2013 +0100
1.3 @@ -1906,6 +1906,47 @@
1.4      by (intro exI[of _ "D - {-t}"]) auto
1.5  qed
1.6
1.7 +lemma inj_setminus: "inj_on uminus (A::'a set set)"
1.8 +  by (auto simp: inj_on_def)
1.9 +
1.10 +lemma compact_fip:
1.11 +  "compact U \<longleftrightarrow>
1.12 +    (\<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> {})"
1.13 +  (is "_ \<longleftrightarrow> ?R")
1.14 +proof (safe intro!: compact_eq_heine_borel[THEN iffD2])
1.15 +  fix A
1.16 +  assume "compact U"
1.17 +    and A: "\<forall>a\<in>A. closed a" "U \<inter> \<Inter>A = {}"
1.18 +    and fi: "\<forall>B \<subseteq> A. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {}"
1.19 +  from A have "(\<forall>a\<in>uminus`A. open a) \<and> U \<subseteq> \<Union>(uminus`A)"
1.20 +    by auto
1.21 +  with `compact U` obtain B where "B \<subseteq> A" "finite (uminus`B)" "U \<subseteq> \<Union>(uminus`B)"
1.22 +    unfolding compact_eq_heine_borel by (metis subset_image_iff)
1.23 +  with fi[THEN spec, of B] show False
1.24 +    by (auto dest: finite_imageD intro: inj_setminus)
1.25 +next
1.26 +  fix A
1.27 +  assume ?R
1.28 +  assume "\<forall>a\<in>A. open a" "U \<subseteq> \<Union>A"
1.29 +  then have "U \<inter> \<Inter>(uminus`A) = {}" "\<forall>a\<in>uminus`A. closed a"
1.30 +    by auto
1.31 +  with `?R` obtain B where "B \<subseteq> A" "finite (uminus`B)" "U \<inter> \<Inter>(uminus`B) = {}"
1.32 +    by (metis subset_image_iff)
1.33 +  then show "\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T"
1.34 +    by  (auto intro!: exI[of _ B] inj_setminus dest: finite_imageD)
1.35 +qed
1.36 +
1.37 +lemma compact_imp_fip:
1.38 +  "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>
1.39 +    s \<inter> (\<Inter> f) \<noteq> {}"
1.40 +  unfolding compact_fip by auto
1.41 +
1.42 +lemma compact_imp_fip_image:
1.43 +  "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>
1.44 +    s \<inter> (\<Inter>i\<in>I. f i) \<noteq> {}"
1.45 +  using finite_subset_image[of _ f I] compact_imp_fip[of s "f`I"] unfolding ball_simps[symmetric] INF_def
1.46 +  by (metis image_iff)
1.47 +
1.48  end
1.49
1.50  lemma (in t2_space) compact_imp_closed:
```