src/HOL/Topological_Spaces.thy
changeset 56166 9a241bc276cd
parent 56020 f92479477c52
child 56231 b98813774a63
     1.1 --- a/src/HOL/Topological_Spaces.thy	Sat Mar 15 16:54:32 2014 +0100
     1.2 +++ b/src/HOL/Topological_Spaces.thy	Sun Mar 16 18:09:04 2014 +0100
     1.3 @@ -31,13 +31,13 @@
     1.4    using open_Union [of "{S, T}"] by simp
     1.5  
     1.6  lemma open_UN [intro]: "\<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Union>x\<in>A. B x)"
     1.7 -  unfolding SUP_def by (rule open_Union) auto
     1.8 +  using open_Union [of "B ` A"] by simp
     1.9  
    1.10  lemma open_Inter [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. open T \<Longrightarrow> open (\<Inter>S)"
    1.11    by (induct set: finite) auto
    1.12  
    1.13  lemma open_INT [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Inter>x\<in>A. B x)"
    1.14 -  unfolding INF_def by (rule open_Inter) auto
    1.15 +  using open_Inter [of "B ` A"] by simp
    1.16  
    1.17  lemma openI:
    1.18    assumes "\<And>x. x \<in> S \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S"
    1.19 @@ -70,7 +70,7 @@
    1.20    by (induct set: finite) auto
    1.21  
    1.22  lemma closed_UN [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Union>x\<in>A. B x)"
    1.23 -  unfolding SUP_def by (rule closed_Union) auto
    1.24 +  using closed_Union [of "B ` A"] by simp
    1.25  
    1.26  lemma open_closed: "open S \<longleftrightarrow> closed (- S)"
    1.27    unfolding closed_def by simp
    1.28 @@ -169,7 +169,7 @@
    1.29  
    1.30  lemma generate_topology_Union: 
    1.31    "(\<And>k. k \<in> I \<Longrightarrow> generate_topology S (K k)) \<Longrightarrow> generate_topology S (\<Union>k\<in>I. K k)"
    1.32 -  unfolding SUP_def by (intro generate_topology.UN) auto
    1.33 +  using generate_topology.UN [of "K ` I"] by auto
    1.34  
    1.35  lemma topological_space_generate_topology:
    1.36    "class.topological_space (generate_topology S)"
    1.37 @@ -1952,10 +1952,25 @@
    1.38    unfolding compact_fip by auto
    1.39  
    1.40  lemma compact_imp_fip_image:
    1.41 -  "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.42 -    s \<inter> (\<Inter>i\<in>I. f i) \<noteq> {}"
    1.43 -  using finite_subset_image[of _ f I] compact_imp_fip[of s "f`I"] unfolding ball_simps[symmetric] INF_def
    1.44 -  by (metis image_iff)
    1.45 +  assumes "compact s"
    1.46 +    and P: "\<And>i. i \<in> I \<Longrightarrow> closed (f i)"
    1.47 +    and Q: "\<And>I'. finite I' \<Longrightarrow> I' \<subseteq> I \<Longrightarrow> (s \<inter> (\<Inter>i\<in>I'. f i) \<noteq> {})"
    1.48 +  shows "s \<inter> (\<Inter>i\<in>I. f i) \<noteq> {}"
    1.49 +proof -
    1.50 +  note `compact s`
    1.51 +  moreover from P have "\<forall>i \<in> f ` I. closed i" by blast
    1.52 +  moreover have "\<forall>A. finite A \<and> A \<subseteq> f ` I \<longrightarrow> (s \<inter> (\<Inter>A) \<noteq> {})"
    1.53 +  proof (rule, rule, erule conjE)
    1.54 +    fix A :: "'a set set"
    1.55 +    assume "finite A"
    1.56 +    moreover assume "A \<subseteq> f ` I"
    1.57 +    ultimately obtain B where "B \<subseteq> I" and "finite B" and "A = f ` B"
    1.58 +      using finite_subset_image [of A f I] by blast
    1.59 +    with Q [of B] show "s \<inter> \<Inter>A \<noteq> {}" by simp
    1.60 +  qed
    1.61 +  ultimately have "s \<inter> (\<Inter>(f ` I)) \<noteq> {}" by (rule compact_imp_fip)
    1.62 +  then show ?thesis by simp
    1.63 +qed
    1.64  
    1.65  end
    1.66