src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
 changeset 53255 addd7b9b2bff parent 53015 a1119cf551e8 child 53282 9d6e263fa921
```     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 28 23:48:45 2013 +0200
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 29 00:18:02 2013 +0200
1.3 @@ -49,6 +49,7 @@
1.4      continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)"
1.5    by (rule continuous_on_If) auto
1.6
1.7 +
1.8  subsection {* Topological Basis *}
1.9
1.10  context topological_space
1.11 @@ -117,41 +118,51 @@
1.12    by (simp add: topological_basis_def)
1.13
1.14  lemma topological_basis_imp_subbasis:
1.15 -  assumes B: "topological_basis B" shows "open = generate_topology B"
1.16 +  assumes B: "topological_basis B"
1.17 +  shows "open = generate_topology B"
1.18  proof (intro ext iffI)
1.19 -  fix S :: "'a set" assume "open S"
1.20 +  fix S :: "'a set"
1.21 +  assume "open S"
1.22    with B obtain B' where "B' \<subseteq> B" "S = \<Union>B'"
1.23      unfolding topological_basis_def by blast
1.24    then show "generate_topology B S"
1.25      by (auto intro: generate_topology.intros dest: topological_basis_open)
1.26  next
1.27 -  fix S :: "'a set" assume "generate_topology B S" then show "open S"
1.28 +  fix S :: "'a set"
1.29 +  assume "generate_topology B S"
1.30 +  then show "open S"
1.31      by induct (auto dest: topological_basis_open[OF B])
1.32  qed
1.33
1.34  lemma basis_dense:
1.35 -  fixes B::"'a set set" and f::"'a set \<Rightarrow> 'a"
1.36 +  fixes B::"'a set set"
1.37 +    and f::"'a set \<Rightarrow> 'a"
1.38    assumes "topological_basis B"
1.39 -  assumes choosefrom_basis: "\<And>B'. B' \<noteq> {} \<Longrightarrow> f B' \<in> B'"
1.40 +    and choosefrom_basis: "\<And>B'. B' \<noteq> {} \<Longrightarrow> f B' \<in> B'"
1.41    shows "(\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>B' \<in> B. f B' \<in> X))"
1.42  proof (intro allI impI)
1.43 -  fix X::"'a set" assume "open X" "X \<noteq> {}"
1.44 +  fix X::"'a set"
1.45 +  assume "open X" "X \<noteq> {}"
1.46    from topological_basisE[OF `topological_basis B` `open X` choosefrom_basis[OF `X \<noteq> {}`]]
1.47    guess B' . note B' = this
1.48 -  thus "\<exists>B'\<in>B. f B' \<in> X" by (auto intro!: choosefrom_basis)
1.49 +  then show "\<exists>B'\<in>B. f B' \<in> X"
1.50 +    by (auto intro!: choosefrom_basis)
1.51  qed
1.52
1.53  end
1.54
1.55  lemma topological_basis_prod:
1.56 -  assumes A: "topological_basis A" and B: "topological_basis B"
1.57 +  assumes A: "topological_basis A"
1.58 +    and B: "topological_basis B"
1.59    shows "topological_basis ((\<lambda>(a, b). a \<times> b) ` (A \<times> B))"
1.60    unfolding topological_basis_def
1.61  proof (safe, simp_all del: ex_simps add: subset_image_iff ex_simps(1)[symmetric])
1.62 -  fix S :: "('a \<times> 'b) set" assume "open S"
1.63 +  fix S :: "('a \<times> 'b) set"
1.64 +  assume "open S"
1.65    then show "\<exists>X\<subseteq>A \<times> B. (\<Union>(a,b)\<in>X. a \<times> b) = S"
1.66    proof (safe intro!: exI[of _ "{x\<in>A \<times> B. fst x \<times> snd x \<subseteq> S}"])
1.67 -    fix x y assume "(x, y) \<in> S"
1.68 +    fix x y
1.69 +    assume "(x, y) \<in> S"
1.70      from open_prod_elim[OF `open S` this]
1.71      obtain a b where a: "open a""x \<in> a" and b: "open b" "y \<in> b" and "a \<times> b \<subseteq> S"
1.72        by (metis mem_Sigma_iff)
1.73 @@ -162,6 +173,7 @@
1.74    qed auto
1.75  qed (metis A B topological_basis_open open_Times)
1.76
1.77 +
1.78  subsection {* Countable Basis *}
1.79
1.80  locale countable_basis =
1.81 @@ -173,12 +185,14 @@
1.82  lemma open_countable_basis_ex:
1.83    assumes "open X"
1.84    shows "\<exists>B' \<subseteq> B. X = Union B'"
1.85 -  using assms countable_basis is_basis unfolding topological_basis_def by blast
1.86 +  using assms countable_basis is_basis
1.87 +  unfolding topological_basis_def by blast
1.88
1.89  lemma open_countable_basisE:
1.90    assumes "open X"
1.91    obtains B' where "B' \<subseteq> B" "X = Union B'"
1.92 -  using assms open_countable_basis_ex by (atomize_elim) simp
1.93 +  using assms open_countable_basis_ex
1.94 +  by (atomize_elim) simp
1.95
1.96  lemma countable_dense_exists:
1.97    shows "\<exists>D::'a set. countable D \<and> (\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>d \<in> D. d \<in> X))"
1.98 @@ -213,34 +227,47 @@
1.99  proof atomize_elim
1.100    from first_countable_basisE[of x] guess A' . note A' = this
1.101    def A \<equiv> "(\<lambda>N. \<Inter>((\<lambda>n. from_nat_into A' n) ` N)) ` (Collect finite::nat set set)"
1.102 -  thus "\<exists>A. countable A \<and> (\<forall>a. a \<in> A \<longrightarrow> x \<in> a) \<and> (\<forall>a. a \<in> A \<longrightarrow> open a) \<and>
1.103 +  then show "\<exists>A. countable A \<and> (\<forall>a. a \<in> A \<longrightarrow> x \<in> a) \<and> (\<forall>a. a \<in> A \<longrightarrow> open a) \<and>
1.104          (\<forall>S. open S \<longrightarrow> x \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)) \<and> (\<forall>a b. a \<in> A \<longrightarrow> b \<in> A \<longrightarrow> a \<inter> b \<in> A)"
1.105    proof (safe intro!: exI[where x=A])
1.106 -    show "countable A" unfolding A_def by (intro countable_image countable_Collect_finite)
1.107 -    fix a assume "a \<in> A"
1.108 -    thus "x \<in> a" "open a" using A'(4)[OF open_UNIV] by (auto simp: A_def intro: A' from_nat_into)
1.109 +    show "countable A"
1.110 +      unfolding A_def by (intro countable_image countable_Collect_finite)
1.111 +    fix a
1.112 +    assume "a \<in> A"
1.113 +    then show "x \<in> a" "open a"
1.114 +      using A'(4)[OF open_UNIV] by (auto simp: A_def intro: A' from_nat_into)
1.115    next
1.116      let ?int = "\<lambda>N. \<Inter>(from_nat_into A' ` N)"
1.117 -    fix a b assume "a \<in> A" "b \<in> A"
1.118 -    then obtain N M where "a = ?int N" "b = ?int M" "finite (N \<union> M)" by (auto simp: A_def)
1.119 -    thus "a \<inter> b \<in> A" by (auto simp: A_def intro!: image_eqI[where x="N \<union> M"])
1.120 +    fix a b
1.121 +    assume "a \<in> A" "b \<in> A"
1.122 +    then obtain N M where "a = ?int N" "b = ?int M" "finite (N \<union> M)"
1.123 +      by (auto simp: A_def)
1.124 +    then show "a \<inter> b \<in> A"
1.125 +      by (auto simp: A_def intro!: image_eqI[where x="N \<union> M"])
1.126    next
1.127 -    fix S assume "open S" "x \<in> S" then obtain a where a: "a\<in>A'" "a \<subseteq> S" using A' by blast
1.128 -    thus "\<exists>a\<in>A. a \<subseteq> S" using a A'
1.129 +    fix S
1.130 +    assume "open S" "x \<in> S"
1.131 +    then obtain a where a: "a\<in>A'" "a \<subseteq> S" using A' by blast
1.132 +    then show "\<exists>a\<in>A. a \<subseteq> S" using a A'
1.133        by (intro bexI[where x=a]) (auto simp: A_def intro: image_eqI[where x="{to_nat_on A' a}"])
1.134    qed
1.135  qed
1.136
1.137  lemma (in topological_space) first_countableI:
1.138 -  assumes "countable A" and 1: "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a"
1.139 -   and 2: "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>a\<in>A. a \<subseteq> S"
1.140 +  assumes "countable A"
1.141 +    and 1: "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a"
1.142 +    and 2: "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>a\<in>A. a \<subseteq> S"
1.143    shows "\<exists>A::nat \<Rightarrow> 'a set. (\<forall>i. x \<in> A i \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))"
1.144  proof (safe intro!: exI[of _ "from_nat_into A"])
1.145 +  fix i
1.146    have "A \<noteq> {}" using 2[of UNIV] by auto
1.147 -  { fix i show "x \<in> from_nat_into A i" "open (from_nat_into A i)"
1.148 -      using range_from_nat_into_subset[OF `A \<noteq> {}`] 1 by auto }
1.149 -  { fix S assume "open S" "x\<in>S" from 2[OF this] show "\<exists>i. from_nat_into A i \<subseteq> S"
1.150 -      using subset_range_from_nat_into[OF `countable A`] by auto }
1.151 +  show "x \<in> from_nat_into A i" "open (from_nat_into A i)"
1.152 +    using range_from_nat_into_subset[OF `A \<noteq> {}`] 1 by auto
1.153 +next
1.154 +  fix S
1.155 +  assume "open S" "x\<in>S" from 2[OF this]
1.156 +  show "\<exists>i. from_nat_into A i \<subseteq> S"
1.157 +    using subset_range_from_nat_into[OF `countable A`] by auto
1.158  qed
1.159
1.160  instance prod :: (first_countable_topology, first_countable_topology) first_countable_topology
1.161 @@ -250,11 +277,13 @@
1.162    from first_countable_basisE[of "snd x"] guess B :: "'b set set" . note B = this
1.163    show "\<exists>A::nat \<Rightarrow> ('a \<times> 'b) set. (\<forall>i. x \<in> A i \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))"
1.164    proof (rule first_countableI[of "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"], safe)
1.165 -    fix a b assume x: "a \<in> A" "b \<in> B"
1.166 +    fix a b
1.167 +    assume x: "a \<in> A" "b \<in> B"
1.168      with A(2, 3)[of a] B(2, 3)[of b] show "x \<in> a \<times> b" "open (a \<times> b)"
1.169        unfolding mem_Times_iff by (auto intro: open_Times)
1.170    next
1.171 -    fix S assume "open S" "x \<in> S"
1.172 +    fix S
1.173 +    assume "open S" "x \<in> S"
1.174      from open_prod_elim[OF this] guess a' b' .
1.175      moreover with A(4)[of a'] B(4)[of b']
1.176      obtain a b where "a \<in> A" "a \<subseteq> a'" "b \<in> B" "b \<subseteq> b'" by auto
1.177 @@ -269,18 +298,22 @@
1.178
1.179  lemma ex_countable_basis: "\<exists>B::'a set set. countable B \<and> topological_basis B"
1.180  proof -
1.181 -  from ex_countable_subbasis obtain B where B: "countable B" "open = generate_topology B" by blast
1.182 +  from ex_countable_subbasis obtain B where B: "countable B" "open = generate_topology B"
1.183 +    by blast
1.184    let ?B = "Inter ` {b. finite b \<and> b \<subseteq> B }"
1.185
1.186    show ?thesis
1.187    proof (intro exI conjI)
1.188      show "countable ?B"
1.189        by (intro countable_image countable_Collect_finite_subset B)
1.190 -    { fix S assume "open S"
1.191 +    {
1.192 +      fix S
1.193 +      assume "open S"
1.194        then have "\<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. (\<Union>b\<in>B'. \<Inter>b) = S"
1.195          unfolding B
1.196        proof induct
1.197 -        case UNIV show ?case by (intro exI[of _ "{{}}"]) simp
1.198 +        case UNIV
1.199 +        show ?case by (intro exI[of _ "{{}}"]) simp
1.200        next
1.201          case (Int a b)
1.202          then obtain x y where x: "a = UNION x Inter" "\<And>i. i \<in> x \<Longrightarrow> finite i \<and> i \<subseteq> B"
1.203 @@ -296,7 +329,8 @@
1.204          then show "\<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. UNION B' Inter = \<Union>K"
1.205            by (intro exI[of _ "UNION K k"]) auto
1.206        next
1.207 -        case (Basis S) then show ?case
1.208 +        case (Basis S)
1.209 +        then show ?case
1.210            by (intro exI[of _ "{{S}}"]) auto
1.211        qed
1.212        then have "(\<exists>B'\<subseteq>Inter ` {b. finite b \<and> b \<subseteq> B}. \<Union>B' = S)"
1.213 @@ -339,6 +373,7 @@
1.214         (fastforce simp: topological_space_class.topological_basis_def)+
1.215  qed
1.216
1.217 +
1.218  subsection {* Polish spaces *}
1.219
1.220  text {* Textbooks define Polish spaces as completely metrizable.
1.221 @@ -348,7 +383,9 @@
1.222
1.223  subsection {* General notion of a topology as a value *}
1.224
1.225 -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.226 +definition "istopology L \<longleftrightarrow>
1.227 +  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.228 +
1.229  typedef 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
1.230    morphisms "openin" "topology"
1.231    unfolding istopology_def by blast
1.232 @@ -363,16 +400,14 @@
1.233    using topology_inverse[of U] istopology_open_in[of "topology U"] by auto
1.234
1.235  lemma topology_eq: "T1 = T2 \<longleftrightarrow> (\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S)"
1.236 -proof-
1.237 -  { assume "T1=T2"
1.238 -    hence "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S" by simp }
1.239 -  moreover
1.240 -  { assume H: "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S"
1.241 -    hence "openin T1 = openin T2" by (simp add: fun_eq_iff)
1.242 -    hence "topology (openin T1) = topology (openin T2)" by simp
1.243 -    hence "T1 = T2" unfolding openin_inverse .
1.244 -  }
1.245 -  ultimately show ?thesis by blast
1.246 +proof
1.247 +  assume "T1 = T2"
1.248 +  then show "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S" by simp
1.249 +next
1.250 +  assume H: "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S"
1.251 +  then have "openin T1 = openin T2" by (simp add: fun_eq_iff)
1.252 +  then have "topology (openin T1) = topology (openin T2)" by simp
1.253 +  then show "T1 = T2" unfolding openin_inverse .
1.254  qed
1.255
1.256  text{* Infer the "universe" from union of all sets in the topology. *}
1.257 @@ -391,7 +426,9 @@
1.258
1.259  lemma openin_subset[intro]: "openin U S \<Longrightarrow> S \<subseteq> topspace U"
1.260    unfolding topspace_def by blast
1.261 -lemma openin_empty[simp]: "openin U {}" by (simp add: openin_clauses)
1.262 +
1.263 +lemma openin_empty[simp]: "openin U {}"
1.264 +  by (simp add: openin_clauses)
1.265
1.266  lemma openin_Int[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<inter> T)"
1.267    using openin_clauses by simp
1.268 @@ -402,7 +439,8 @@
1.269  lemma openin_Un[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<union> T)"
1.270    using openin_Union[of "{S,T}" U] by auto
1.271
1.272 -lemma openin_topspace[intro, simp]: "openin U (topspace U)" by (simp add: openin_Union topspace_def)
1.273 +lemma openin_topspace[intro, simp]: "openin U (topspace U)"
1.274 +  by (simp add: openin_Union topspace_def)
1.275
1.276  lemma openin_subopen: "openin U S \<longleftrightarrow> (\<forall>x \<in> S. \<exists>T. openin U T \<and> x \<in> T \<and> T \<subseteq> S)"
1.277    (is "?lhs \<longleftrightarrow> ?rhs")
1.278 @@ -422,42 +460,63 @@
1.279
1.280  definition "closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U - S)"
1.281
1.282 -lemma closedin_subset: "closedin U S \<Longrightarrow> S \<subseteq> topspace U" by (metis closedin_def)
1.283 -lemma closedin_empty[simp]: "closedin U {}" by (simp add: closedin_def)
1.284 -lemma closedin_topspace[intro,simp]:
1.285 -  "closedin U (topspace U)" by (simp add: closedin_def)
1.286 +lemma closedin_subset: "closedin U S \<Longrightarrow> S \<subseteq> topspace U"
1.287 +  by (metis closedin_def)
1.288 +
1.289 +lemma closedin_empty[simp]: "closedin U {}"
1.290 +  by (simp add: closedin_def)
1.291 +
1.292 +lemma closedin_topspace[intro, simp]: "closedin U (topspace U)"
1.293 +  by (simp add: closedin_def)
1.294 +
1.295  lemma closedin_Un[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<union> T)"
1.296    by (auto simp add: Diff_Un closedin_def)
1.297
1.298 -lemma Diff_Inter[intro]: "A - \<Inter>S = \<Union> {A - s|s. s\<in>S}" by auto
1.299 -lemma closedin_Inter[intro]: assumes Ke: "K \<noteq> {}" and Kc: "\<forall>S \<in>K. closedin U S"
1.300 -  shows "closedin U (\<Inter> K)"  using Ke Kc unfolding closedin_def Diff_Inter by auto
1.301 +lemma Diff_Inter[intro]: "A - \<Inter>S = \<Union> {A - s|s. s\<in>S}"
1.302 +  by auto
1.303 +
1.304 +lemma closedin_Inter[intro]:
1.305 +  assumes Ke: "K \<noteq> {}"
1.306 +    and Kc: "\<forall>S \<in>K. closedin U S"
1.307 +  shows "closedin U (\<Inter> K)"
1.308 +  using Ke Kc unfolding closedin_def Diff_Inter by auto
1.309
1.310  lemma closedin_Int[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<inter> T)"
1.311    using closedin_Inter[of "{S,T}" U] by auto
1.312
1.313 -lemma Diff_Diff_Int: "A - (A - B) = A \<inter> B" by blast
1.314 +lemma Diff_Diff_Int: "A - (A - B) = A \<inter> B"
1.315 +  by blast
1.316 +
1.317  lemma openin_closedin_eq: "openin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> closedin U (topspace U - S)"
1.318    apply (auto simp add: closedin_def Diff_Diff_Int inf_absorb2)
1.319    apply (metis openin_subset subset_eq)
1.320    done
1.321
1.322 -lemma openin_closedin:  "S \<subseteq> topspace U \<Longrightarrow> (openin U S \<longleftrightarrow> closedin U (topspace U - S))"
1.323 +lemma openin_closedin: "S \<subseteq> topspace U \<Longrightarrow> (openin U S \<longleftrightarrow> closedin U (topspace U - S))"
1.324    by (simp add: openin_closedin_eq)
1.325
1.326 -lemma openin_diff[intro]: assumes oS: "openin U S" and cT: "closedin U T" shows "openin U (S - T)"
1.327 -proof-
1.328 +lemma openin_diff[intro]:
1.329 +  assumes oS: "openin U S"
1.330 +    and cT: "closedin U T"
1.331 +  shows "openin U (S - T)"
1.332 +proof -
1.333    have "S - T = S \<inter> (topspace U - T)" using openin_subset[of U S]  oS cT
1.334      by (auto simp add: topspace_def openin_subset)
1.335    then show ?thesis using oS cT by (auto simp add: closedin_def)
1.336  qed
1.337
1.338 -lemma closedin_diff[intro]: assumes oS: "closedin U S" and cT: "openin U T" shows "closedin U (S - T)"
1.339 -proof-
1.340 -  have "S - T = S \<inter> (topspace U - T)" using closedin_subset[of U S]  oS cT
1.341 -    by (auto simp add: topspace_def )
1.342 -  then show ?thesis using oS cT by (auto simp add: openin_closedin_eq)
1.343 -qed
1.344 +lemma closedin_diff[intro]:
1.345 +  assumes oS: "closedin U S"
1.346 +    and cT: "openin U T"
1.347 +  shows "closedin U (S - T)"
1.348 +proof -
1.349 +  have "S - T = S \<inter> (topspace U - T)"
1.350 +    using closedin_subset[of U S] oS cT
1.351 +    by (auto simp add: topspace_def)
1.352 +  then show ?thesis
1.353 +    using oS cT by (auto simp add: openin_closedin_eq)
1.354 +qed
1.355 +
1.356
1.357  subsubsection {* Subspace topology *}
1.358
1.359 @@ -465,48 +524,59 @@
1.360
1.361  lemma istopology_subtopology: "istopology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
1.362    (is "istopology ?L")
1.363 -proof-
1.364 +proof -
1.365    have "?L {}" by blast
1.366 -  {fix A B assume A: "?L A" and B: "?L B"
1.367 -    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.368 -    have "A\<inter>B = (Sa \<inter> Sb) \<inter> V" "openin U (Sa \<inter> Sb)"  using Sa Sb by blast+
1.369 -    then have "?L (A \<inter> B)" by blast}
1.370 +  {
1.371 +    fix A B
1.372 +    assume A: "?L A" and B: "?L B"
1.373 +    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"
1.374 +      by blast
1.375 +    have "A \<inter> B = (Sa \<inter> Sb) \<inter> V" "openin U (Sa \<inter> Sb)"
1.376 +      using Sa Sb by blast+
1.377 +    then have "?L (A \<inter> B)" by blast
1.378 +  }
1.379    moreover
1.380 -  {fix K assume K: "K \<subseteq> Collect ?L"
1.381 +  {
1.382 +    fix K assume K: "K \<subseteq> Collect ?L"
1.383      have th0: "Collect ?L = (\<lambda>S. S \<inter> V) ` Collect (openin U)"
1.384        apply (rule set_eqI)
1.385        apply (simp add: Ball_def image_iff)
1.386 -      by metis
1.387 +      apply metis
1.388 +      done
1.389      from K[unfolded th0 subset_image_iff]
1.390 -    obtain Sk where Sk: "Sk \<subseteq> Collect (openin U)" "K = (\<lambda>S. S \<inter> V) ` Sk" by blast
1.391 -    have "\<Union>K = (\<Union>Sk) \<inter> V" using Sk by auto
1.392 -    moreover have "openin U (\<Union> Sk)" using Sk by (auto simp add: subset_eq)
1.393 -    ultimately have "?L (\<Union>K)" by blast}
1.394 +    obtain Sk where Sk: "Sk \<subseteq> Collect (openin U)" "K = (\<lambda>S. S \<inter> V) ` Sk"
1.395 +      by blast
1.396 +    have "\<Union>K = (\<Union>Sk) \<inter> V"
1.397 +      using Sk by auto
1.398 +    moreover have "openin U (\<Union> Sk)"
1.399 +      using Sk by (auto simp add: subset_eq)
1.400 +    ultimately have "?L (\<Union>K)" by blast
1.401 +  }
1.402    ultimately show ?thesis
1.403      unfolding subset_eq mem_Collect_eq istopology_def by blast
1.404  qed
1.405
1.406 -lemma openin_subtopology:
1.407 -  "openin (subtopology U V) S \<longleftrightarrow> (\<exists> T. (openin U T) \<and> (S = T \<inter> V))"
1.408 +lemma openin_subtopology: "openin (subtopology U V) S \<longleftrightarrow> (\<exists>T. openin U T \<and> S = T \<inter> V)"
1.409    unfolding subtopology_def topology_inverse'[OF istopology_subtopology]
1.410    by auto
1.411
1.412 -lemma topspace_subtopology: "topspace(subtopology U V) = topspace U \<inter> V"
1.413 +lemma topspace_subtopology: "topspace (subtopology U V) = topspace U \<inter> V"
1.414    by (auto simp add: topspace_def openin_subtopology)
1.415
1.416 -lemma closedin_subtopology:
1.417 -  "closedin (subtopology U V) S \<longleftrightarrow> (\<exists>T. closedin U T \<and> S = T \<inter> V)"
1.418 +lemma closedin_subtopology: "closedin (subtopology U V) S \<longleftrightarrow> (\<exists>T. closedin U T \<and> S = T \<inter> V)"
1.419    unfolding closedin_def topspace_subtopology
1.420    apply (simp add: openin_subtopology)
1.421    apply (rule iffI)
1.422    apply clarify
1.423    apply (rule_tac x="topspace U - T" in exI)
1.424 -  by auto
1.425 +  apply auto
1.426 +  done
1.427
1.428  lemma openin_subtopology_refl: "openin (subtopology U V) V \<longleftrightarrow> V \<subseteq> topspace U"
1.429    unfolding openin_subtopology
1.430    apply (rule iffI, clarify)
1.431 -  apply (frule openin_subset[of U])  apply blast
1.432 +  apply (frule openin_subset[of U])
1.433 +  apply blast
1.434    apply (rule exI[where x="topspace U"])
1.435    apply auto
1.436    done
1.437 @@ -514,17 +584,28 @@
1.438  lemma subtopology_superset:
1.439    assumes UV: "topspace U \<subseteq> V"
1.440    shows "subtopology U V = U"
1.441 -proof-
1.442 -  {fix S
1.443 -    {fix T assume T: "openin U T" "S = T \<inter> V"
1.444 -      from T openin_subset[OF T(1)] UV have eq: "S = T" by blast
1.445 -      have "openin U S" unfolding eq using T by blast}
1.446 +proof -
1.447 +  {
1.448 +    fix S
1.449 +    {
1.450 +      fix T
1.451 +      assume T: "openin U T" "S = T \<inter> V"
1.452 +      from T openin_subset[OF T(1)] UV have eq: "S = T"
1.453 +        by blast
1.454 +      have "openin U S"
1.455 +        unfolding eq using T by blast
1.456 +    }
1.457      moreover
1.458 -    {assume S: "openin U S"
1.459 -      hence "\<exists>T. openin U T \<and> S = T \<inter> V"
1.460 -        using openin_subset[OF S] UV by auto}
1.461 -    ultimately have "(\<exists>T. openin U T \<and> S = T \<inter> V) \<longleftrightarrow> openin U S" by blast}
1.462 -  then show ?thesis unfolding topology_eq openin_subtopology by blast
1.463 +    {
1.464 +      assume S: "openin U S"
1.465 +      then have "\<exists>T. openin U T \<and> S = T \<inter> V"
1.466 +        using openin_subset[OF S] UV by auto
1.467 +    }
1.468 +    ultimately have "(\<exists>T. openin U T \<and> S = T \<inter> V) \<longleftrightarrow> openin U S"
1.469 +      by blast
1.470 +  }
1.471 +  then show ?thesis
1.472 +    unfolding topology_eq openin_subtopology by blast
1.473  qed
1.474
1.475  lemma subtopology_topspace[simp]: "subtopology U (topspace U) = U"
1.476 @@ -533,11 +614,11 @@
1.477  lemma subtopology_UNIV[simp]: "subtopology U UNIV = U"
1.478    by (simp add: subtopology_superset)
1.479
1.480 +
1.481  subsubsection {* The standard Euclidean topology *}
1.482
1.483 -definition
1.484 -  euclidean :: "'a::topological_space topology" where
1.485 -  "euclidean = topology open"
1.486 +definition euclidean :: "'a::topological_space topology"
1.487 +  where "euclidean = topology open"
1.488
1.489  lemma open_openin: "open S \<longleftrightarrow> openin euclidean S"
1.490    unfolding euclidean_def
1.491 @@ -549,7 +630,8 @@
1.492  lemma topspace_euclidean: "topspace euclidean = UNIV"
1.493    apply (simp add: topspace_def)
1.494    apply (rule set_eqI)
1.495 -  by (auto simp add: open_openin[symmetric])
1.496 +  apply (auto simp add: open_openin[symmetric])
1.497 +  done
1.498
1.499  lemma topspace_euclidean_subtopology[simp]: "topspace (subtopology euclidean S) = S"
1.500    by (simp add: topspace_euclidean topspace_subtopology)
1.501 @@ -569,10 +651,10 @@
1.502    by (auto simp add: openin_open)
1.503
1.504  lemma open_openin_trans[trans]:
1.505 - "open S \<Longrightarrow> open T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> openin (subtopology euclidean S) T"
1.506 +  "open S \<Longrightarrow> open T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> openin (subtopology euclidean S) T"
1.507    by (metis Int_absorb1  openin_open_Int)
1.508
1.509 -lemma open_subset:  "S \<subseteq> T \<Longrightarrow> open S \<Longrightarrow> openin (subtopology euclidean T) S"
1.510 +lemma open_subset: "S \<subseteq> T \<Longrightarrow> open S \<Longrightarrow> openin (subtopology euclidean T) S"
1.511    by (auto simp add: openin_open)
1.512
1.513  lemma closedin_closed: "closedin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. closed T \<and> S = U \<inter> T)"
1.514 @@ -593,10 +675,12 @@
1.515
1.516  lemma openin_euclidean_subtopology_iff:
1.517    fixes S U :: "'a::metric_space set"
1.518 -  shows "openin (subtopology euclidean U) S
1.519 -  \<longleftrightarrow> S \<subseteq> U \<and> (\<forall>x\<in>S. \<exists>e>0. \<forall>x'\<in>U. dist x' x < e \<longrightarrow> x'\<in> S)" (is "?lhs \<longleftrightarrow> ?rhs")
1.520 +  shows "openin (subtopology euclidean U) S \<longleftrightarrow>
1.521 +    S \<subseteq> U \<and> (\<forall>x\<in>S. \<exists>e>0. \<forall>x'\<in>U. dist x' x < e \<longrightarrow> x'\<in> S)"
1.522 +  (is "?lhs \<longleftrightarrow> ?rhs")
1.523  proof
1.524 -  assume ?lhs thus ?rhs unfolding openin_open open_dist by blast
1.525 +  assume ?lhs
1.526 +  then show ?rhs unfolding openin_open open_dist by blast
1.527  next
1.528    def T \<equiv> "{x. \<exists>a\<in>S. \<exists>d>0. (\<forall>y\<in>U. dist y a < d \<longrightarrow> y \<in> S) \<and> dist x a < d}"
1.529    have 1: "\<forall>x\<in>T. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> T"
1.530 @@ -620,17 +704,17 @@
1.531
1.532  text {* These "transitivity" results are handy too *}
1.533
1.534 -lemma openin_trans[trans]: "openin (subtopology euclidean T) S \<Longrightarrow> openin (subtopology euclidean U) T
1.535 -  \<Longrightarrow> openin (subtopology euclidean U) S"
1.536 +lemma openin_trans[trans]:
1.537 +  "openin (subtopology euclidean T) S \<Longrightarrow> openin (subtopology euclidean U) T \<Longrightarrow>
1.538 +    openin (subtopology euclidean U) S"
1.539    unfolding open_openin openin_open by blast
1.540
1.541  lemma openin_open_trans: "openin (subtopology euclidean T) S \<Longrightarrow> open T \<Longrightarrow> open S"
1.542    by (auto simp add: openin_open intro: openin_trans)
1.543
1.544  lemma closedin_trans[trans]:
1.545 - "closedin (subtopology euclidean T) S \<Longrightarrow>
1.546 -           closedin (subtopology euclidean U) T
1.547 -           ==> closedin (subtopology euclidean U) S"
1.548 +  "closedin (subtopology euclidean T) S \<Longrightarrow> closedin (subtopology euclidean U) T \<Longrightarrow>
1.549 +    closedin (subtopology euclidean U) S"
1.550    by (auto simp add: closedin_closed closed_closedin closed_Inter Int_assoc)
1.551
1.552  lemma closedin_closed_trans: "closedin (subtopology euclidean T) S \<Longrightarrow> closed T \<Longrightarrow> closed S"
1.553 @@ -639,13 +723,11 @@
1.554
1.555  subsection {* Open and closed balls *}
1.556
1.557 -definition
1.558 -  ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" where
1.559 -  "ball x e = {y. dist x y < e}"
1.560 -
1.561 -definition
1.562 -  cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" where
1.563 -  "cball x e = {y. dist x y \<le> e}"
1.564 +definition ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
1.565 +  where "ball x e = {y. dist x y < e}"
1.566 +
1.567 +definition cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
1.568 +  where "cball x e = {y. dist x y \<le> e}"
1.569
1.570  lemma mem_ball [simp]: "y \<in> ball x e \<longleftrightarrow> dist x y < e"
1.571    by (simp add: ball_def)
1.572 @@ -669,20 +751,33 @@
1.573  lemma centre_in_cball: "x \<in> cball x e \<longleftrightarrow> 0 \<le> e"
1.574    by simp
1.575
1.576 -lemma ball_subset_cball[simp,intro]: "ball x e \<subseteq> cball x e" by (simp add: subset_eq)
1.577 -lemma subset_ball[intro]: "d <= e ==> ball x d \<subseteq> ball x e" by (simp add: subset_eq)
1.578 -lemma subset_cball[intro]: "d <= e ==> cball x d \<subseteq> cball x e" by (simp add: subset_eq)
1.579 +lemma ball_subset_cball[simp,intro]: "ball x e \<subseteq> cball x e"
1.580 +  by (simp add: subset_eq)
1.581 +
1.582 +lemma subset_ball[intro]: "d <= e ==> ball x d \<subseteq> ball x e"
1.583 +  by (simp add: subset_eq)
1.584 +
1.585 +lemma subset_cball[intro]: "d <= e ==> cball x d \<subseteq> cball x e"
1.586 +  by (simp add: subset_eq)
1.587 +
1.588  lemma ball_max_Un: "ball a (max r s) = ball a r \<union> ball a s"
1.589    by (simp add: set_eq_iff) arith
1.590
1.591  lemma ball_min_Int: "ball a (min r s) = ball a r \<inter> ball a s"
1.592    by (simp add: set_eq_iff)
1.593
1.594 -lemma diff_less_iff: "(a::real) - b > 0 \<longleftrightarrow> a > b"
1.595 +lemma diff_less_iff:
1.596 +  "(a::real) - b > 0 \<longleftrightarrow> a > b"
1.597    "(a::real) - b < 0 \<longleftrightarrow> a < b"
1.598 -  "a - b < c \<longleftrightarrow> a < c +b" "a - b > c \<longleftrightarrow> a > c +b" by arith+
1.599 -lemma diff_le_iff: "(a::real) - b \<ge> 0 \<longleftrightarrow> a \<ge> b" "(a::real) - b \<le> 0 \<longleftrightarrow> a \<le> b"
1.600 -  "a - b \<le> c \<longleftrightarrow> a \<le> c +b" "a - b \<ge> c \<longleftrightarrow> a \<ge> c +b"  by arith+
1.601 +  "a - b < c \<longleftrightarrow> a < c + b" "a - b > c \<longleftrightarrow> a > c + b"
1.602 +  by arith+
1.603 +
1.604 +lemma diff_le_iff:
1.605 +  "(a::real) - b \<ge> 0 \<longleftrightarrow> a \<ge> b"
1.606 +  "(a::real) - b \<le> 0 \<longleftrightarrow> a \<le> b"
1.607 +  "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
1.608 +  "a - b \<ge> c \<longleftrightarrow> a \<ge> c + b"
1.609 +  by arith+
1.610
1.611  lemma open_ball[intro, simp]: "open (ball x e)"
1.612    unfolding open_dist ball_def mem_Collect_eq Ball_def
1.613 @@ -730,30 +825,41 @@
1.614    shows "\<exists>a b. (\<forall>i\<in>Basis. a \<bullet> i \<in> \<rat> \<and> b \<bullet> i \<in> \<rat> ) \<and> x \<in> box a b \<and> box a b \<subseteq> ball x e"
1.615  proof -
1.616    def e' \<equiv> "e / (2 * sqrt (real (DIM ('a))))"
1.617 -  then have e: "0 < e'" using assms by (auto intro!: divide_pos_pos simp: DIM_positive)
1.618 +  then have e: "0 < e'"
1.619 +    using assms by (auto intro!: divide_pos_pos simp: DIM_positive)
1.620    have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x \<bullet> i \<and> x \<bullet> i - y < e'" (is "\<forall>i. ?th i")
1.621    proof
1.622 -    fix i from Rats_dense_in_real[of "x \<bullet> i - e'" "x \<bullet> i"] e show "?th i" by auto
1.623 +    fix i
1.624 +    from Rats_dense_in_real[of "x \<bullet> i - e'" "x \<bullet> i"] e
1.625 +    show "?th i" by auto
1.626    qed
1.627    from choice[OF this] guess a .. note a = this
1.628    have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x \<bullet> i < y \<and> y - x \<bullet> i < e'" (is "\<forall>i. ?th i")
1.629    proof
1.630 -    fix i from Rats_dense_in_real[of "x \<bullet> i" "x \<bullet> i + e'"] e show "?th i" by auto
1.631 +    fix i
1.632 +    from Rats_dense_in_real[of "x \<bullet> i" "x \<bullet> i + e'"] e
1.633 +    show "?th i" by auto
1.634    qed
1.635    from choice[OF this] guess b .. note b = this
1.636    let ?a = "\<Sum>i\<in>Basis. a i *\<^sub>R i" and ?b = "\<Sum>i\<in>Basis. b i *\<^sub>R i"
1.637    show ?thesis
1.638    proof (rule exI[of _ ?a], rule exI[of _ ?b], safe)
1.639 -    fix y :: 'a assume *: "y \<in> box ?a ?b"
1.640 +    fix y :: 'a
1.641 +    assume *: "y \<in> box ?a ?b"
1.642      have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)"
1.643        unfolding setL2_def[symmetric] by (rule euclidean_dist_l2)
1.644      also have "\<dots> < sqrt (\<Sum>(i::'a)\<in>Basis. e^2 / real (DIM('a)))"
1.645      proof (rule real_sqrt_less_mono, rule setsum_strict_mono)
1.646 -      fix i :: "'a" assume i: "i \<in> Basis"
1.647 -      have "a i < y\<bullet>i \<and> y\<bullet>i < b i" using * i by (auto simp: box_def)
1.648 -      moreover have "a i < x\<bullet>i" "x\<bullet>i - a i < e'" using a by auto
1.649 -      moreover have "x\<bullet>i < b i" "b i - x\<bullet>i < e'" using b by auto
1.650 -      ultimately have "\<bar>x\<bullet>i - y\<bullet>i\<bar> < 2 * e'" by auto
1.651 +      fix i :: "'a"
1.652 +      assume i: "i \<in> Basis"
1.653 +      have "a i < y\<bullet>i \<and> y\<bullet>i < b i"
1.654 +        using * i by (auto simp: box_def)
1.655 +      moreover have "a i < x\<bullet>i" "x\<bullet>i - a i < e'"
1.656 +        using a by auto
1.657 +      moreover have "x\<bullet>i < b i" "b i - x\<bullet>i < e'"
1.658 +        using b by auto
1.659 +      ultimately have "\<bar>x\<bullet>i - y\<bullet>i\<bar> < 2 * e'"
1.660 +        by auto
1.661        then have "dist (x \<bullet> i) (y \<bullet> i) < e/sqrt (real (DIM('a)))"
1.662          unfolding e'_def by (auto simp: dist_real_def)
1.663        then have "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < (e/sqrt (real (DIM('a))))\<^sup>2"
1.664 @@ -761,8 +867,10 @@
1.665        then show "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < e\<^sup>2 / real DIM('a)"
1.666          by (simp add: power_divide)
1.667      qed auto
1.668 -    also have "\<dots> = e" using `0 < e` by (simp add: real_eq_of_nat)
1.669 -    finally show "y \<in> ball x e" by (auto simp: ball_def)
1.670 +    also have "\<dots> = e"
1.671 +      using `0 < e` by (simp add: real_eq_of_nat)
1.672 +    finally show "y \<in> ball x e"
1.673 +      by (auto simp: ball_def)
1.674    qed (insert a b, auto simp: box_def)
1.675  qed
1.676
1.677 @@ -792,51 +900,67 @@
1.678  subsection{* Connectedness *}
1.679
1.680  lemma connected_local:
1.681 - "connected S \<longleftrightarrow> ~(\<exists>e1 e2.
1.682 -                 openin (subtopology euclidean S) e1 \<and>
1.683 -                 openin (subtopology euclidean S) e2 \<and>
1.684 -                 S \<subseteq> e1 \<union> e2 \<and>
1.685 -                 e1 \<inter> e2 = {} \<and>
1.686 -                 ~(e1 = {}) \<and>
1.687 -                 ~(e2 = {}))"
1.688 -unfolding connected_def openin_open by (safe, blast+)
1.689 + "connected S \<longleftrightarrow>
1.690 +  \<not> (\<exists>e1 e2.
1.691 +      openin (subtopology euclidean S) e1 \<and>
1.692 +      openin (subtopology euclidean S) e2 \<and>
1.693 +      S \<subseteq> e1 \<union> e2 \<and>
1.694 +      e1 \<inter> e2 = {} \<and>
1.695 +      e1 \<noteq> {} \<and>
1.696 +      e2 \<noteq> {})"
1.697 +  unfolding connected_def openin_open by (safe, blast+)
1.698
1.699  lemma exists_diff:
1.700    fixes P :: "'a set \<Rightarrow> bool"
1.701    shows "(\<exists>S. P(- S)) \<longleftrightarrow> (\<exists>S. P S)" (is "?lhs \<longleftrightarrow> ?rhs")
1.702 -proof-
1.703 -  {assume "?lhs" hence ?rhs by blast }
1.704 +proof -
1.705 +  {
1.706 +    assume "?lhs"
1.707 +    then have ?rhs by blast
1.708 +  }
1.709    moreover
1.710 -  {fix S assume H: "P S"
1.711 +  {
1.712 +    fix S
1.713 +    assume H: "P S"
1.714      have "S = - (- S)" by auto
1.715 -    with H have "P (- (- S))" by metis }
1.716 +    with H have "P (- (- S))" by metis
1.717 +  }
1.718    ultimately show ?thesis by metis
1.719  qed
1.720
1.721  lemma connected_clopen: "connected S \<longleftrightarrow>
1.722 -        (\<forall>T. openin (subtopology euclidean S) T \<and>
1.723 -            closedin (subtopology euclidean S) T \<longrightarrow> T = {} \<or> T = S)" (is "?lhs \<longleftrightarrow> ?rhs")
1.724 -proof-
1.725 -  have " \<not> connected S \<longleftrightarrow> (\<exists>e1 e2. open e1 \<and> open (- e2) \<and> S \<subseteq> e1 \<union> (- e2) \<and> e1 \<inter> (- e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (- e2) \<inter> S \<noteq> {})"
1.726 +  (\<forall>T. openin (subtopology euclidean S) T \<and>
1.727 +     closedin (subtopology euclidean S) T \<longrightarrow> T = {} \<or> T = S)" (is "?lhs \<longleftrightarrow> ?rhs")
1.728 +proof -
1.729 +  have "\<not> connected S \<longleftrightarrow>
1.730 +    (\<exists>e1 e2. open e1 \<and> open (- e2) \<and> S \<subseteq> e1 \<union> (- e2) \<and> e1 \<inter> (- e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (- e2) \<inter> S \<noteq> {})"
1.731      unfolding connected_def openin_open closedin_closed
1.732      apply (subst exists_diff)
1.733      apply blast
1.734      done
1.735 -  hence th0: "connected S \<longleftrightarrow> \<not> (\<exists>e2 e1. closed e2 \<and> open e1 \<and> S \<subseteq> e1 \<union> (- e2) \<and> e1 \<inter> (- e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (- e2) \<inter> S \<noteq> {})"
1.736 +  hence th0: "connected S \<longleftrightarrow>
1.737 +    \<not> (\<exists>e2 e1. closed e2 \<and> open e1 \<and> S \<subseteq> e1 \<union> (- e2) \<and> e1 \<inter> (- e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (- e2) \<inter> S \<noteq> {})"
1.738      (is " _ \<longleftrightarrow> \<not> (\<exists>e2 e1. ?P e2 e1)")
1.739      apply (simp add: closed_def)
1.740      apply metis
1.741      done
1.742 -
1.743    have th1: "?rhs \<longleftrightarrow> \<not> (\<exists>t' t. closed t'\<and>t = S\<inter>t' \<and> t\<noteq>{} \<and> t\<noteq>S \<and> (\<exists>t'. open t' \<and> t = S \<inter> t'))"
1.744      (is "_ \<longleftrightarrow> \<not> (\<exists>t' t. ?Q t' t)")
1.745      unfolding connected_def openin_open closedin_closed by auto
1.746 -  {fix e2
1.747 -    {fix e1 have "?P e2 e1 \<longleftrightarrow> (\<exists>t.  closed e2 \<and> t = S\<inter>e2 \<and> open e1 \<and> t = S\<inter>e1 \<and> t\<noteq>{} \<and> t\<noteq>S)"
1.748 -        by auto}
1.749 -    then have "(\<exists>e1. ?P e2 e1) \<longleftrightarrow> (\<exists>t. ?Q e2 t)" by metis}
1.750 -  then have "\<forall>e2. (\<exists>e1. ?P e2 e1) \<longleftrightarrow> (\<exists>t. ?Q e2 t)" by blast
1.751 -  then show ?thesis unfolding th0 th1 by simp
1.752 +  {
1.753 +    fix e2
1.754 +    {
1.755 +      fix e1
1.756 +      have "?P e2 e1 \<longleftrightarrow> (\<exists>t.  closed e2 \<and> t = S\<inter>e2 \<and> open e1 \<and> t = S\<inter>e1 \<and> t\<noteq>{} \<and> t\<noteq>S)"
1.757 +        by auto
1.758 +    }
1.759 +    then have "(\<exists>e1. ?P e2 e1) \<longleftrightarrow> (\<exists>t. ?Q e2 t)"
1.760 +      by metis
1.761 +  }
1.762 +  then have "\<forall>e2. (\<exists>e1. ?P e2 e1) \<longleftrightarrow> (\<exists>t. ?Q e2 t)"
1.763 +    by blast
1.764 +  then show ?thesis
1.765 +    unfolding th0 th1 by simp
1.766  qed
1.767
1.768  lemma connected_empty[simp, intro]: "connected {}"  (* FIXME duplicate? *)
1.769 @@ -845,9 +969,8 @@
1.770
1.771  subsection{* Limit points *}
1.772
1.773 -definition (in topological_space)
1.774 -  islimpt:: "'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "islimpt" 60) where
1.775 -  "x islimpt S \<longleftrightarrow> (\<forall>T. x\<in>T \<longrightarrow> open T \<longrightarrow> (\<exists>y\<in>S. y\<in>T \<and> y\<noteq>x))"
1.776 +definition (in topological_space) islimpt:: "'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "islimpt" 60)
1.777 +  where "x islimpt S \<longleftrightarrow> (\<forall>T. x\<in>T \<longrightarrow> open T \<longrightarrow> (\<exists>y\<in>S. y\<in>T \<and> y\<noteq>x))"
1.778
1.779  lemma islimptI:
1.780    assumes "\<And>T. x \<in> T \<Longrightarrow> open T \<Longrightarrow> \<exists>y\<in>S. y \<in> T \<and> y \<noteq> x"
1.781 @@ -862,7 +985,7 @@
1.782  lemma islimpt_iff_eventually: "x islimpt S \<longleftrightarrow> \<not> eventually (\<lambda>y. y \<notin> S) (at x)"
1.783    unfolding islimpt_def eventually_at_topological by auto
1.784
1.785 -lemma islimpt_subset: "\<lbrakk>x islimpt S; S \<subseteq> T\<rbrakk> \<Longrightarrow> x islimpt T"
1.786 +lemma islimpt_subset: "x islimpt S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> x islimpt T"
1.787    unfolding islimpt_def by fast
1.788
1.789  lemma islimpt_approachable:
1.790 @@ -892,8 +1015,8 @@
1.791  lemma perfect_choose_dist:
1.792    fixes x :: "'a::{perfect_space, metric_space}"
1.793    shows "0 < r \<Longrightarrow> \<exists>a. a \<noteq> x \<and> dist a x < r"
1.794 -using islimpt_UNIV [of x]
1.795 -by (simp add: islimpt_approachable)
1.796 +  using islimpt_UNIV [of x]
1.797 +  by (simp add: islimpt_approachable)
1.798
1.799  lemma closed_limpt: "closed S \<longleftrightarrow> (\<forall>x. x islimpt S \<longrightarrow> x \<in> S)"
1.800    unfolding closed_def
1.801 @@ -907,20 +1030,29 @@
1.802
1.803  lemma finite_set_avoid:
1.804    fixes a :: "'a::metric_space"
1.805 -  assumes fS: "finite S" shows  "\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<longrightarrow> d <= dist a x"
1.806 -proof(induct rule: finite_induct[OF fS])
1.807 -  case 1 thus ?case by (auto intro: zero_less_one)
1.808 +  assumes fS: "finite S"
1.809 +  shows  "\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<longrightarrow> d <= dist a x"
1.810 +proof (induct rule: finite_induct[OF fS])
1.811 +  case 1
1.812 +  then show ?case by (auto intro: zero_less_one)
1.813  next
1.814    case (2 x F)
1.815 -  from 2 obtain d where d: "d >0" "\<forall>x\<in>F. x\<noteq>a \<longrightarrow> d \<le> dist a x" by blast
1.816 -  {assume "x = a" hence ?case using d by auto  }
1.817 -  moreover
1.818 -  {assume xa: "x\<noteq>a"
1.819 +  from 2 obtain d where d: "d >0" "\<forall>x\<in>F. x\<noteq>a \<longrightarrow> d \<le> dist a x"
1.820 +    by blast
1.821 +  show ?case
1.822 +  proof (cases "x = a")
1.823 +    case True
1.824 +    then show ?thesis using d by auto
1.825 +  next
1.826 +    case False
1.827      let ?d = "min d (dist a x)"
1.828 -    have dp: "?d > 0" using xa d(1) using dist_nz by auto
1.829 -    from d have d': "\<forall>x\<in>F. x\<noteq>a \<longrightarrow> ?d \<le> dist a x" by auto
1.830 -    with dp xa have ?case by(auto intro!: exI[where x="?d"]) }
1.831 -  ultimately show ?case by blast
1.832 +    have dp: "?d > 0"
1.833 +      using False d(1) using dist_nz by auto
1.834 +    from d have d': "\<forall>x\<in>F. x\<noteq>a \<longrightarrow> ?d \<le> dist a x"
1.835 +      by auto
1.836 +    with dp False show ?thesis
1.837 +      by (auto intro!: exI[where x="?d"])
1.838 +  qed
1.839  qed
1.840
1.841  lemma islimpt_Un: "x islimpt (S \<union> T) \<longleftrightarrow> x islimpt S \<or> x islimpt T"
1.842 @@ -928,20 +1060,27 @@
1.843
1.844  lemma discrete_imp_closed:
1.845    fixes S :: "'a::metric_space set"
1.846 -  assumes e: "0 < e" and d: "\<forall>x \<in> S. \<forall>y \<in> S. dist y x < e \<longrightarrow> y = x"
1.847 +  assumes e: "0 < e"
1.848 +    and d: "\<forall>x \<in> S. \<forall>y \<in> S. dist y x < e \<longrightarrow> y = x"
1.849    shows "closed S"
1.850 -proof-
1.851 -  {fix x assume C: "\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e"
1.852 +proof -
1.853 +  {
1.854 +    fix x
1.855 +    assume C: "\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e"
1.856      from e have e2: "e/2 > 0" by arith
1.857 -    from C[rule_format, OF e2] obtain y where y: "y \<in> S" "y\<noteq>x" "dist y x < e/2" by blast
1.858 +    from C[rule_format, OF e2] obtain y where y: "y \<in> S" "y\<noteq>x" "dist y x < e/2"
1.859 +      by blast
1.860      let ?m = "min (e/2) (dist x y) "
1.861 -    from e2 y(2) have mp: "?m > 0" by (simp add: dist_nz[THEN sym])
1.862 -    from C[rule_format, OF mp] obtain z where z: "z \<in> S" "z\<noteq>x" "dist z x < ?m" by blast
1.863 +    from e2 y(2) have mp: "?m > 0"
1.864 +      by (simp add: dist_nz[THEN sym])
1.865 +    from C[rule_format, OF mp] obtain z where z: "z \<in> S" "z\<noteq>x" "dist z x < ?m"
1.866 +      by blast
1.867      have th: "dist z y < e" using z y
1.868        by (intro dist_triangle_lt [where z=x], simp)
1.869      from d[rule_format, OF y(1) z(1) th] y z
1.870      have False by (auto simp add: dist_commute)}
1.871 -  then show ?thesis by (metis islimpt_approachable closed_limpt [where 'a='a])
1.872 +  then show ?thesis
1.873 +    by (metis islimpt_approachable closed_limpt [where 'a='a])
1.874  qed
1.875
1.876
1.877 @@ -1005,7 +1144,8 @@
1.878
1.879  lemma interior_limit_point [intro]:
1.880    fixes x :: "'a::perfect_space"
1.881 -  assumes x: "x \<in> interior S" shows "x islimpt S"
1.882 +  assumes x: "x \<in> interior S"
1.883 +  shows "x islimpt S"
1.884    using x islimpt_UNIV [of x]
1.885    unfolding interior_def islimpt_def
1.886    apply (clarsimp, rename_tac T T')
1.887 @@ -1014,15 +1154,16 @@
1.888    done
1.889
1.890  lemma interior_closed_Un_empty_interior:
1.891 -  assumes cS: "closed S" and iT: "interior T = {}"
1.892 +  assumes cS: "closed S"
1.893 +    and iT: "interior T = {}"
1.894    shows "interior (S \<union> T) = interior S"
1.895  proof
1.896    show "interior S \<subseteq> interior (S \<union> T)"
1.897 -    by (rule interior_mono, rule Un_upper1)
1.898 -next
1.899 +    by (rule interior_mono) (rule Un_upper1)
1.900    show "interior (S \<union> T) \<subseteq> interior S"
1.901    proof
1.902 -    fix x assume "x \<in> interior (S \<union> T)"
1.903 +    fix x
1.904 +    assume "x \<in> interior (S \<union> T)"
1.905      then obtain R where "open R" "x \<in> R" "R \<subseteq> S \<union> T" ..
1.906      show "x \<in> interior S"
1.907      proof (rule ccontr)
1.908 @@ -1043,14 +1184,17 @@
1.909      by (intro Sigma_mono interior_subset)
1.910    show "open (interior A \<times> interior B)"
1.911      by (intro open_Times open_interior)
1.912 -  fix T assume "T \<subseteq> A \<times> B" and "open T" thus "T \<subseteq> interior A \<times> interior B"
1.913 +  fix T
1.914 +  assume "T \<subseteq> A \<times> B" and "open T"
1.915 +  then show "T \<subseteq> interior A \<times> interior B"
1.916    proof (safe)
1.917 -    fix x y assume "(x, y) \<in> T"
1.918 +    fix x y
1.919 +    assume "(x, y) \<in> T"
1.920      then obtain C D where "open C" "open D" "C \<times> D \<subseteq> T" "x \<in> C" "y \<in> D"
1.921        using `open T` unfolding open_prod_def by fast
1.922 -    hence "open C" "open D" "C \<subseteq> A" "D \<subseteq> B" "x \<in> C" "y \<in> D"
1.923 +    then have "open C" "open D" "C \<subseteq> A" "D \<subseteq> B" "x \<in> C" "y \<in> D"
1.924        using `T \<subseteq> A \<times> B` by auto
1.925 -    thus "x \<in> interior A" and "y \<in> interior B"
1.926 +    then show "x \<in> interior A" and "y \<in> interior B"
1.927        by (auto intro: interiorI)
1.928    qed
1.929  qed
1.930 @@ -1091,8 +1235,9 @@
1.931    unfolding closure_hull by (rule hull_minimal)
1.932
1.933  lemma closure_unique:
1.934 -  assumes "S \<subseteq> T" and "closed T"
1.935 -  assumes "\<And>T'. S \<subseteq> T' \<Longrightarrow> closed T' \<Longrightarrow> T \<subseteq> T'"
1.936 +  assumes "S \<subseteq> T"
1.937 +    and "closed T"
1.938 +    and "\<And>T'. S \<subseteq> T' \<Longrightarrow> closed T' \<Longrightarrow> T \<subseteq> T'"
1.939    shows "closure S = T"
1.940    using assms unfolding closure_hull by (rule hull_unique)
1.941
1.942 @@ -1125,7 +1270,8 @@
1.943  proof
1.944    fix x
1.945    assume as: "open S" "x \<in> S \<inter> closure T"
1.946 -  { assume *:"x islimpt T"
1.947 +  {
1.948 +    assume *:"x islimpt T"
1.949      have "x islimpt (S \<inter> T)"
1.950      proof (rule islimptI)
1.951        fix A
1.952 @@ -1134,9 +1280,9 @@
1.953          by (simp_all add: open_Int)
1.954        with * obtain y where "y \<in> T" "y \<in> A \<inter> S" "y \<noteq> x"
1.955          by (rule islimptE)
1.956 -      hence "y \<in> S \<inter> T" "y \<in> A \<and> y \<noteq> x"
1.957 +      then have "y \<in> S \<inter> T" "y \<in> A \<and> y \<noteq> x"
1.958          by simp_all
1.959 -      thus "\<exists>y\<in>(S \<inter> T). y \<in> A \<and> y \<noteq> x" ..
1.960 +      then show "\<exists>y\<in>(S \<inter> T). y \<in> A \<and> y \<noteq> x" ..
1.961      qed
1.962    }
1.963    then show "x \<in> closure (S \<inter> T)" using as
1.964 @@ -1167,7 +1313,6 @@
1.965      done
1.966  qed
1.967
1.968 -
1.969  lemma islimpt_in_closure: "(x islimpt S) = (x:closure(S-{x}))"
1.970    unfolding closure_def using islimpt_punctured by blast
1.971
1.972 @@ -1176,7 +1321,7 @@
1.973
1.974  definition "frontier S = closure S - interior S"
1.975
1.976 -lemma frontier_closed: "closed(frontier S)"
1.977 +lemma frontier_closed: "closed (frontier S)"
1.978    by (simp add: frontier_def closed_Diff)
1.979
1.980  lemma frontier_closures: "frontier S = (closure S) \<inter> (closure(- S))"
1.981 @@ -1196,11 +1341,14 @@
1.982
1.983  lemma frontier_subset_eq: "frontier S \<subseteq> S \<longleftrightarrow> closed S"
1.984  proof-
1.985 -  { assume "frontier S \<subseteq> S"
1.986 -    hence "closure S \<subseteq> S" using interior_subset unfolding frontier_def by auto
1.987 -    hence "closed S" using closure_subset_eq by auto
1.988 +  {
1.989 +    assume "frontier S \<subseteq> S"
1.990 +    then have "closure S \<subseteq> S"
1.991 +      using interior_subset unfolding frontier_def by auto
1.992 +    then have "closed S"
1.993 +      using closure_subset_eq by auto
1.994    }
1.995 -  thus ?thesis using frontier_subset_closed[of S] ..
1.996 +  then show ?thesis using frontier_subset_closed[of S] ..
1.997  qed
1.998
1.999  lemma frontier_complement: "frontier(- S) = frontier S"
1.1000 @@ -1221,7 +1369,7 @@
1.1001  lemma trivial_limit_within: "trivial_limit (at a within S) \<longleftrightarrow> \<not> a islimpt S"
1.1002  proof
1.1003    assume "trivial_limit (at a within S)"
1.1004 -  thus "\<not> a islimpt S"
1.1005 +  then show "\<not> a islimpt S"
1.1006      unfolding trivial_limit_def
1.1007      unfolding eventually_at_topological
1.1008      unfolding islimpt_def
1.1009 @@ -1231,7 +1379,7 @@
1.1010      done
1.1011  next
1.1012    assume "\<not> a islimpt S"
1.1013 -  thus "trivial_limit (at a within S)"
1.1014 +  then show "trivial_limit (at a within S)"
1.1015      unfolding trivial_limit_def
1.1016      unfolding eventually_at_topological
1.1017      unfolding islimpt_def
1.1018 @@ -1266,9 +1414,9 @@
1.1019
1.1020  lemma eventually_at2:
1.1021    "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
1.1022 -unfolding eventually_at dist_nz by auto
1.1023 -
1.1024 -lemma eventually_happens: "eventually P net ==> trivial_limit net \<or> (\<exists>x. P x)"
1.1025 +  unfolding eventually_at dist_nz by auto
1.1026 +
1.1027 +lemma eventually_happens: "eventually P net \<Longrightarrow> trivial_limit net \<or> (\<exists>x. P x)"
1.1028    unfolding trivial_limit_def
1.1029    by (auto elim: eventually_rev_mp)
1.1030
1.1031 @@ -1282,7 +1430,7 @@
1.1032
1.1033  lemma eventually_rev_mono:
1.1034    "eventually P net \<Longrightarrow> (\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually Q net"
1.1035 -using eventually_mono [of P Q] by fast
1.1036 +  using eventually_mono [of P Q] by fast
1.1037
1.1038  lemma not_eventually: "(\<forall>x. \<not> P x ) \<Longrightarrow> ~(trivial_limit net) ==> ~(eventually (\<lambda>x. P x) net)"
1.1039    by (simp add: eventually_False)
1.1040 @@ -1291,7 +1439,7 @@
1.1041  subsection {* Limits *}
1.1042
1.1043  lemma Lim:
1.1044 - "(f ---> l) net \<longleftrightarrow>
1.1045 +  "(f ---> l) net \<longleftrightarrow>
1.1046          trivial_limit net \<or>
1.1047          (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
1.1048    unfolding tendsto_iff trivial_limit_eq by auto
1.1049 @@ -1322,7 +1470,8 @@
1.1050  lemma Lim_within_empty: "(f ---> l) (at x within {})"
1.1051    unfolding tendsto_def eventually_at_filter by simp
1.1052
1.1053 -lemma Lim_Un: assumes "(f ---> l) (at x within S)" "(f ---> l) (at x within T)"
1.1054 +lemma Lim_Un:
1.1055 +  assumes "(f ---> l) (at x within S)" "(f ---> l) (at x within T)"
1.1056    shows "(f ---> l) (at x within (S \<union> T))"
1.1057    using assms unfolding tendsto_def eventually_at_filter
1.1058    apply clarify
1.1059 @@ -1332,36 +1481,36 @@
1.1060    done
1.1061
1.1062  lemma Lim_Un_univ:
1.1063 - "(f ---> l) (at x within S) \<Longrightarrow> (f ---> l) (at x within T) \<Longrightarrow>  S \<union> T = UNIV
1.1064 -        ==> (f ---> l) (at x)"
1.1065 +  "(f ---> l) (at x within S) \<Longrightarrow> (f ---> l) (at x within T) \<Longrightarrow>
1.1066 +    S \<union> T = UNIV \<Longrightarrow> (f ---> l) (at x)"
1.1067    by (metis Lim_Un)
1.1068
1.1069  text{* Interrelations between restricted and unrestricted limits. *}
1.1070
1.1071 -
1.1072  lemma Lim_at_within: (* FIXME: rename *)
1.1073    "(f ---> l) (at x) \<Longrightarrow> (f ---> l) (at x within S)"
1.1074    by (metis order_refl filterlim_mono subset_UNIV at_le)
1.1075
1.1076  lemma eventually_within_interior:
1.1077    assumes "x \<in> interior S"
1.1078 -  shows "eventually P (at x within S) \<longleftrightarrow> eventually P (at x)" (is "?lhs = ?rhs")
1.1079 -proof -
1.1080 +  shows "eventually P (at x within S) \<longleftrightarrow> eventually P (at x)"
1.1081 +  (is "?lhs = ?rhs")
1.1082 +proof
1.1083    from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S" ..
1.1084 -  { assume "?lhs"
1.1085 +  {
1.1086 +    assume "?lhs"
1.1087      then obtain A where "open A" "x \<in> A" "\<forall>y\<in>A. y \<noteq> x \<longrightarrow> y \<in> S \<longrightarrow> P y"
1.1088        unfolding eventually_at_topological
1.1089        by auto
1.1090      with T have "open (A \<inter> T)" "x \<in> A \<inter> T" "\<forall>y\<in>(A \<inter> T). y \<noteq> x \<longrightarrow> P y"
1.1091        by auto
1.1092 -    then have "?rhs"
1.1093 +    then show "?rhs"
1.1094        unfolding eventually_at_topological by auto
1.1095 -  }
1.1096 -  moreover
1.1097 -  { assume "?rhs" hence "?lhs"
1.1098 +  next
1.1099 +    assume "?rhs"
1.1100 +    then show "?lhs"
1.1101        by (auto elim: eventually_elim1 simp: eventually_at_filter)
1.1102    }
1.1103 -  ultimately show "?thesis" ..
1.1104  qed
1.1105
1.1106  lemma at_within_interior:
1.1107 @@ -1379,24 +1528,31 @@
1.1108    fixes f :: "'a :: {linorder_topology, conditionally_complete_linorder, no_top} \<Rightarrow>
1.1109      'b::{linorder_topology, conditionally_complete_linorder}"
1.1110    assumes mono: "\<And>a b. a \<in> I \<Longrightarrow> b \<in> I \<Longrightarrow> x < a \<Longrightarrow> a \<le> b \<Longrightarrow> f a \<le> f b"
1.1111 -  assumes bnd: "\<And>a. a \<in> I \<Longrightarrow> x < a \<Longrightarrow> K \<le> f a"
1.1112 +    and bnd: "\<And>a. a \<in> I \<Longrightarrow> x < a \<Longrightarrow> K \<le> f a"
1.1113    shows "(f ---> Inf (f ` ({x<..} \<inter> I))) (at x within ({x<..} \<inter> I))"
1.1114  proof cases
1.1115 -  assume "{x<..} \<inter> I = {}" then show ?thesis by (simp add: Lim_within_empty)
1.1116 +  assume "{x<..} \<inter> I = {}"
1.1117 +  then show ?thesis by (simp add: Lim_within_empty)
1.1118  next
1.1119    assume e: "{x<..} \<inter> I \<noteq> {}"
1.1120    show ?thesis
1.1121    proof (rule order_tendstoI)
1.1122      fix a assume a: "a < Inf (f ` ({x<..} \<inter> I))"
1.1123 -    { fix y assume "y \<in> {x<..} \<inter> I"
1.1124 +    {
1.1125 +      fix y
1.1126 +      assume "y \<in> {x<..} \<inter> I"
1.1127        with e bnd have "Inf (f ` ({x<..} \<inter> I)) \<le> f y"
1.1128          by (auto intro: cInf_lower)
1.1129 -      with a have "a < f y" by (blast intro: less_le_trans) }
1.1130 +      with a have "a < f y"
1.1131 +        by (blast intro: less_le_trans)
1.1132 +    }
1.1133      then show "eventually (\<lambda>x. a < f x) (at x within ({x<..} \<inter> I))"
1.1134        by (auto simp: eventually_at_filter intro: exI[of _ 1] zero_less_one)
1.1135    next
1.1136 -    fix a assume "Inf (f ` ({x<..} \<inter> I)) < a"
1.1137 -    from cInf_lessD[OF _ this] e obtain y where y: "x < y" "y \<in> I" "f y < a" by auto
1.1138 +    fix a
1.1139 +    assume "Inf (f ` ({x<..} \<inter> I)) < a"
1.1140 +    from cInf_lessD[OF _ this] e obtain y where y: "x < y" "y \<in> I" "f y < a"
1.1141 +      by auto
1.1142      then have "eventually (\<lambda>x. x \<in> I \<longrightarrow> f x < a) (at_right x)"
1.1143        unfolding eventually_at_right by (metis less_imp_le le_less_trans mono)
1.1144      then show "eventually (\<lambda>x. f x < a) (at x within ({x<..} \<inter> I))"
1.1145 @@ -1414,27 +1570,33 @@
1.1146    assume ?lhs
1.1147    from countable_basis_at_decseq[of x] guess A . note A = this
1.1148    def f \<equiv> "\<lambda>n. SOME y. y \<in> S \<and> y \<in> A n \<and> x \<noteq> y"
1.1149 -  { fix n
1.1150 +  {
1.1151 +    fix n
1.1152      from `?lhs` have "\<exists>y. y \<in> S \<and> y \<in> A n \<and> x \<noteq> y"
1.1153        unfolding islimpt_def using A(1,2)[of n] by auto
1.1154      then have "f n \<in> S \<and> f n \<in> A n \<and> x \<noteq> f n"
1.1155        unfolding f_def by (rule someI_ex)
1.1156 -    then have "f n \<in> S" "f n \<in> A n" "x \<noteq> f n" by auto }
1.1157 +    then have "f n \<in> S" "f n \<in> A n" "x \<noteq> f n" by auto
1.1158 +  }
1.1159    then have "\<forall>n. f n \<in> S - {x}" by auto
1.1160    moreover have "(\<lambda>n. f n) ----> x"
1.1161    proof (rule topological_tendstoI)
1.1162 -    fix S assume "open S" "x \<in> S"
1.1163 +    fix S
1.1164 +    assume "open S" "x \<in> S"
1.1165      from A(3)[OF this] `\<And>n. f n \<in> A n`
1.1166 -    show "eventually (\<lambda>x. f x \<in> S) sequentially" by (auto elim!: eventually_elim1)
1.1167 +    show "eventually (\<lambda>x. f x \<in> S) sequentially"
1.1168 +      by (auto elim!: eventually_elim1)
1.1169    qed
1.1170    ultimately show ?rhs by fast
1.1171  next
1.1172    assume ?rhs
1.1173 -  then obtain f :: "nat \<Rightarrow> 'a" where f: "\<And>n. f n \<in> S - {x}" and lim: "f ----> x" by auto
1.1174 +  then obtain f :: "nat \<Rightarrow> 'a" where f: "\<And>n. f n \<in> S - {x}" and lim: "f ----> x"
1.1175 +    by auto
1.1176    show ?lhs
1.1177      unfolding islimpt_def
1.1178    proof safe
1.1179 -    fix T assume "open T" "x \<in> T"
1.1180 +    fix T
1.1181 +    assume "open T" "x \<in> T"
1.1182      from lim[THEN topological_tendstoD, OF this] f
1.1183      show "\<exists>y\<in>S. y \<in> T \<and> y \<noteq> x"
1.1184        unfolding eventually_sequentially by auto
1.1185 @@ -1442,8 +1604,10 @@
1.1186  qed
1.1187
1.1188  lemma Lim_inv: (* TODO: delete *)
1.1189 -  fixes f :: "'a \<Rightarrow> real" and A :: "'a filter"
1.1190 -  assumes "(f ---> l) A" and "l \<noteq> 0"
1.1191 +  fixes f :: "'a \<Rightarrow> real"
1.1192 +    and A :: "'a filter"
1.1193 +  assumes "(f ---> l) A"
1.1194 +    and "l \<noteq> 0"
1.1195    shows "((inverse o f) ---> inverse l) A"
1.1196    unfolding o_def using assms by (rule tendsto_inverse)
1.1197
1.1198 @@ -1459,13 +1623,14 @@
1.1199  proof (rule metric_tendsto_imp_tendsto)
1.1200    show "(g ---> 0) net" by fact
1.1201    show "eventually (\<lambda>x. dist (f x) 0 \<le> dist (g x) 0) net"
1.1202 -    using assms(1) by (rule eventually_elim1, simp add: dist_norm)
1.1203 +    using assms(1) by (rule eventually_elim1) (simp add: dist_norm)
1.1204  qed
1.1205
1.1206  lemma Lim_transform_bound:
1.1207    fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
1.1208 -  fixes g :: "'a \<Rightarrow> 'c::real_normed_vector"
1.1209 -  assumes "eventually (\<lambda>n. norm(f n) <= norm(g n)) net"  "(g ---> 0) net"
1.1210 +    and g :: "'a \<Rightarrow> 'c::real_normed_vector"
1.1211 +  assumes "eventually (\<lambda>n. norm(f n) <= norm(g n)) net"
1.1212 +    and "(g ---> 0) net"
1.1213    shows "(f ---> 0) net"
1.1214    using assms(1) tendsto_norm_zero [OF assms(2)]
1.1215    by (rule Lim_null_comparison)
1.1216 @@ -1473,7 +1638,9 @@
1.1217  text{* Deducing things about the limit from the elements. *}
1.1218
1.1219  lemma Lim_in_closed_set:
1.1220 -  assumes "closed S" "eventually (\<lambda>x. f(x) \<in> S) net" "\<not>(trivial_limit net)" "(f ---> l) net"
1.1221 +  assumes "closed S"
1.1222 +    and "eventually (\<lambda>x. f(x) \<in> S) net"
1.1223 +    and "\<not>(trivial_limit net)" "(f ---> l) net"
1.1224    shows "l \<in> S"
1.1225  proof (rule ccontr)
1.1226    assume "l \<notin> S"
1.1227 @@ -1490,32 +1657,42 @@
1.1228  text{* Need to prove closed(cball(x,e)) before deducing this as a corollary. *}
1.1229
1.1230  lemma Lim_dist_ubound:
1.1231 -  assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. dist a (f x) <= e) net"
1.1232 +  assumes "\<not>(trivial_limit net)"
1.1233 +    and "(f ---> l) net"
1.1234 +    and "eventually (\<lambda>x. dist a (f x) <= e) net"
1.1235    shows "dist a l <= e"
1.1236  proof -
1.1237    have "dist a l \<in> {..e}"
1.1238    proof (rule Lim_in_closed_set)
1.1239 -    show "closed {..e}" by simp
1.1240 -    show "eventually (\<lambda>x. dist a (f x) \<in> {..e}) net" by (simp add: assms)
1.1241 -    show "\<not> trivial_limit net" by fact
1.1242 -    show "((\<lambda>x. dist a (f x)) ---> dist a l) net" by (intro tendsto_intros assms)
1.1243 +    show "closed {..e}"
1.1244 +      by simp
1.1245 +    show "eventually (\<lambda>x. dist a (f x) \<in> {..e}) net"
1.1246 +      by (simp add: assms)
1.1247 +    show "\<not> trivial_limit net"
1.1248 +      by fact
1.1249 +    show "((\<lambda>x. dist a (f x)) ---> dist a l) net"
1.1250 +      by (intro tendsto_intros assms)
1.1251    qed
1.1252 -  thus ?thesis by simp
1.1253 +  then show ?thesis by simp
1.1254  qed
1.1255
1.1256  lemma Lim_norm_ubound:
1.1257    fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
1.1258 -  assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. norm(f x) <= e) net"
1.1259 -  shows "norm(l) <= e"
1.1260 +  assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. norm(f x) \<le> e) net"
1.1261 +  shows "norm(l) \<le> e"
1.1262  proof -
1.1263    have "norm l \<in> {..e}"
1.1264    proof (rule Lim_in_closed_set)
1.1265 -    show "closed {..e}" by simp
1.1266 -    show "eventually (\<lambda>x. norm (f x) \<in> {..e}) net" by (simp add: assms)
1.1267 -    show "\<not> trivial_limit net" by fact
1.1268 -    show "((\<lambda>x. norm (f x)) ---> norm l) net" by (intro tendsto_intros assms)
1.1269 +    show "closed {..e}"
1.1270 +      by simp
1.1271 +    show "eventually (\<lambda>x. norm (f x) \<in> {..e}) net"
1.1272 +      by (simp add: assms)
1.1273 +    show "\<not> trivial_limit net"
1.1274 +      by fact
1.1275 +    show "((\<lambda>x. norm (f x)) ---> norm l) net"
1.1276 +      by (intro tendsto_intros assms)
1.1277    qed
1.1278 -  thus ?thesis by simp
1.1279 +  then show ?thesis by simp
1.1280  qed
1.1281
1.1282  lemma Lim_norm_lbound:
1.1283 @@ -1525,12 +1702,16 @@
1.1284  proof -
1.1285    have "norm l \<in> {e..}"
1.1286    proof (rule Lim_in_closed_set)
1.1287 -    show "closed {e..}" by simp
1.1288 -    show "eventually (\<lambda>x. norm (f x) \<in> {e..}) net" by (simp add: assms)
1.1289 -    show "\<not> trivial_limit net" by fact
1.1290 -    show "((\<lambda>x. norm (f x)) ---> norm l) net" by (intro tendsto_intros assms)
1.1291 +    show "closed {e..}"
1.1292 +      by simp
1.1293 +    show "eventually (\<lambda>x. norm (f x) \<in> {e..}) net"
1.1294 +      by (simp add: assms)
1.1295 +    show "\<not> trivial_limit net"
1.1296 +      by fact
1.1297 +    show "((\<lambda>x. norm (f x)) ---> norm l) net"
1.1298 +      by (intro tendsto_intros assms)
1.1299    qed
1.1300 -  thus ?thesis by simp
1.1301 +  then show ?thesis by simp
1.1302  qed
1.1303
1.1304  text{* Limit under bilinear function *}
```