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
```