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: