src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 44170 510ac30f44c0
parent 44167 e81d676d598e
child 44207 ea99698c2070
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Aug 12 07:18:28 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Aug 12 09:17:24 2011 -0700
     1.3 @@ -22,8 +22,8 @@
     1.4  
     1.5  subsection{* General notion of a topology *}
     1.6  
     1.7 -definition "istopology L \<longleftrightarrow> {} \<in> L \<and> (\<forall>S \<in>L. \<forall>T \<in>L. S \<inter> T \<in> L) \<and> (\<forall>K. K \<subseteq>L \<longrightarrow> \<Union> K \<in> L)"
     1.8 -typedef (open) 'a topology = "{L::('a set) set. istopology L}"
     1.9 +definition "istopology L \<longleftrightarrow> L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union> K))"
    1.10 +typedef (open) 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
    1.11    morphisms "openin" "topology"
    1.12    unfolding istopology_def by blast
    1.13  
    1.14 @@ -31,7 +31,7 @@
    1.15    using openin[of U] by blast
    1.16  
    1.17  lemma topology_inverse': "istopology U \<Longrightarrow> openin (topology U) = U"
    1.18 -  using topology_inverse[unfolded mem_def Collect_def] .
    1.19 +  using topology_inverse[unfolded mem_Collect_eq] .
    1.20  
    1.21  lemma topology_inverse_iff: "istopology U \<longleftrightarrow> openin (topology U) = U"
    1.22    using topology_inverse[of U] istopology_open_in[of "topology U"] by auto
    1.23 @@ -41,7 +41,7 @@
    1.24    {assume "T1=T2" hence "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S" by simp}
    1.25    moreover
    1.26    {assume H: "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S"
    1.27 -    hence "openin T1 = openin T2" by (metis mem_def set_eqI)
    1.28 +    hence "openin T1 = openin T2" by (simp add: fun_eq_iff)
    1.29      hence "topology (openin T1) = topology (openin T2)" by simp
    1.30      hence "T1 = T2" unfolding openin_inverse .}
    1.31    ultimately show ?thesis by blast
    1.32 @@ -58,8 +58,8 @@
    1.33    shows "openin U {}"
    1.34    "\<And>S T. openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S\<inter>T)"
    1.35    "\<And>K. (\<forall>S \<in> K. openin U S) \<Longrightarrow> openin U (\<Union>K)"
    1.36 -  using openin[of U] unfolding istopology_def Collect_def mem_def
    1.37 -  unfolding subset_eq Ball_def mem_def by auto
    1.38 +  using openin[of U] unfolding istopology_def mem_Collect_eq
    1.39 +  by fast+
    1.40  
    1.41  lemma openin_subset[intro]: "openin U S \<Longrightarrow> S \<subseteq> topspace U"
    1.42    unfolding topspace_def by blast
    1.43 @@ -130,33 +130,38 @@
    1.44  
    1.45  subsection{* Subspace topology. *}
    1.46  
    1.47 -definition "subtopology U V = topology {S \<inter> V |S. openin U S}"
    1.48 -
    1.49 -lemma istopology_subtopology: "istopology {S \<inter> V |S. openin U S}" (is "istopology ?L")
    1.50 +term "{f x |x. P x}"
    1.51 +term "{y. \<exists>x. y = f x \<and> P x}"
    1.52 +
    1.53 +definition "subtopology U V = topology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
    1.54 +
    1.55 +lemma istopology_subtopology: "istopology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
    1.56 +  (is "istopology ?L")
    1.57  proof-
    1.58 -  have "{} \<in> ?L" by blast
    1.59 -  {fix A B assume A: "A \<in> ?L" and B: "B \<in> ?L"
    1.60 +  have "?L {}" by blast
    1.61 +  {fix A B assume A: "?L A" and B: "?L B"
    1.62      from A B obtain Sa and Sb where Sa: "openin U Sa" "A = Sa \<inter> V" and Sb: "openin U Sb" "B = Sb \<inter> V" by blast
    1.63      have "A\<inter>B = (Sa \<inter> Sb) \<inter> V" "openin U (Sa \<inter> Sb)"  using Sa Sb by blast+
    1.64 -    then have "A \<inter> B \<in> ?L" by blast}
    1.65 +    then have "?L (A \<inter> B)" by blast}
    1.66    moreover
    1.67 -  {fix K assume K: "K \<subseteq> ?L"
    1.68 -    have th0: "?L = (\<lambda>S. S \<inter> V) ` openin U "
    1.69 +  {fix K assume K: "K \<subseteq> Collect ?L"
    1.70 +    have th0: "Collect ?L = (\<lambda>S. S \<inter> V) ` Collect (openin U)"
    1.71        apply (rule set_eqI)
    1.72        apply (simp add: Ball_def image_iff)
    1.73 -      by (metis mem_def)
    1.74 +      by metis
    1.75      from K[unfolded th0 subset_image_iff]
    1.76 -    obtain Sk where Sk: "Sk \<subseteq> openin U" "K = (\<lambda>S. S \<inter> V) ` Sk" by blast
    1.77 +    obtain Sk where Sk: "Sk \<subseteq> Collect (openin U)" "K = (\<lambda>S. S \<inter> V) ` Sk" by blast
    1.78      have "\<Union>K = (\<Union>Sk) \<inter> V" using Sk by auto
    1.79 -    moreover have "openin U (\<Union> Sk)" using Sk by (auto simp add: subset_eq mem_def)
    1.80 -    ultimately have "\<Union>K \<in> ?L" by blast}
    1.81 -  ultimately show ?thesis unfolding istopology_def by blast
    1.82 +    moreover have "openin U (\<Union> Sk)" using Sk by (auto simp add: subset_eq)
    1.83 +    ultimately have "?L (\<Union>K)" by blast}
    1.84 +  ultimately show ?thesis
    1.85 +    unfolding subset_eq mem_Collect_eq istopology_def by blast
    1.86  qed
    1.87  
    1.88  lemma openin_subtopology:
    1.89    "openin (subtopology U V) S \<longleftrightarrow> (\<exists> T. (openin U T) \<and> (S = T \<inter> V))"
    1.90    unfolding subtopology_def topology_inverse'[OF istopology_subtopology]
    1.91 -  by (auto simp add: Collect_def)
    1.92 +  by auto
    1.93  
    1.94  lemma topspace_subtopology: "topspace(subtopology U V) = topspace U \<inter> V"
    1.95    by (auto simp add: topspace_def openin_subtopology)
    1.96 @@ -210,7 +215,7 @@
    1.97    apply (rule cong[where x=S and y=S])
    1.98    apply (rule topology_inverse[symmetric])
    1.99    apply (auto simp add: istopology_def)
   1.100 -  by (auto simp add: mem_def subset_eq)
   1.101 +  done
   1.102  
   1.103  lemma topspace_euclidean: "topspace euclidean = UNIV"
   1.104    apply (simp add: topspace_def)
   1.105 @@ -266,7 +271,7 @@
   1.106    "a - b \<le> c \<longleftrightarrow> a \<le> c +b" "a - b \<ge> c \<longleftrightarrow> a \<ge> c +b"  by arith+
   1.107  
   1.108  lemma open_ball[intro, simp]: "open (ball x e)"
   1.109 -  unfolding open_dist ball_def Collect_def Ball_def mem_def
   1.110 +  unfolding open_dist ball_def mem_Collect_eq Ball_def
   1.111    unfolding dist_commute
   1.112    apply clarify
   1.113    apply (rule_tac x="e - dist xa x" in exI)
   1.114 @@ -492,7 +497,7 @@
   1.115    unfolding closed_def
   1.116    apply (subst open_subopen)
   1.117    apply (simp add: islimpt_def subset_eq)
   1.118 -  by (metis ComplE ComplI insertCI insert_absorb mem_def)
   1.119 +  by (metis ComplE ComplI)
   1.120  
   1.121  lemma islimpt_EMPTY[simp]: "\<not> x islimpt {}"
   1.122    unfolding islimpt_def by auto
   1.123 @@ -691,14 +696,13 @@
   1.124    }
   1.125    ultimately show ?thesis
   1.126      using hull_unique[of S, of "closure S", of closed]
   1.127 -    unfolding mem_def
   1.128      by simp
   1.129  qed
   1.130  
   1.131  lemma closure_eq: "closure S = S \<longleftrightarrow> closed S"
   1.132    unfolding closure_hull
   1.133 -  using hull_eq[of closed, unfolded mem_def, OF  closed_Inter, of S]
   1.134 -  by (metis mem_def subset_eq)
   1.135 +  using hull_eq[of closed, OF  closed_Inter, of S]
   1.136 +  by metis
   1.137  
   1.138  lemma closure_closed[simp]: "closed S \<Longrightarrow> closure S = S"
   1.139    using closure_eq[of S]
   1.140 @@ -721,12 +725,12 @@
   1.141  
   1.142  lemma closure_minimal: "S \<subseteq> T \<Longrightarrow>  closed T \<Longrightarrow> closure S \<subseteq> T"
   1.143    using hull_minimal[of S T closed]
   1.144 -  unfolding closure_hull mem_def
   1.145 +  unfolding closure_hull
   1.146    by simp
   1.147  
   1.148  lemma closure_unique: "S \<subseteq> T \<and> closed T \<and> (\<forall> T'. S \<subseteq> T' \<and> closed T' \<longrightarrow> T \<subseteq> T') \<Longrightarrow> closure S = T"
   1.149    using hull_unique[of S T closed]
   1.150 -  unfolding closure_hull mem_def
   1.151 +  unfolding closure_hull
   1.152    by simp
   1.153  
   1.154  lemma closure_empty[simp]: "closure {} = {}"
   1.155 @@ -1623,7 +1627,7 @@
   1.156  qed
   1.157  
   1.158  lemma open_contains_cball_eq: "open S ==> (\<forall>x. x \<in> S \<longleftrightarrow> (\<exists>e>0. cball x e \<subseteq> S))"
   1.159 -  by (metis open_contains_cball subset_eq order_less_imp_le centre_in_cball mem_def)
   1.160 +  by (metis open_contains_cball subset_eq order_less_imp_le centre_in_cball)
   1.161  
   1.162  lemma mem_interior_cball: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. cball x e \<subseteq> S)"
   1.163    apply (simp add: interior_def, safe)