author huffman Sat Jun 06 09:11:12 2009 -0700 (2009-06-06) changeset 31488 5691ccb8d6b5 parent 31487 93938cafc0e6 child 31489 10080e31b294
generalize tendsto to class topological_space
 src/HOL/Library/Topology_Euclidean_Space.thy file | annotate | diff | revisions src/HOL/Lim.thy file | annotate | diff | revisions src/HOL/Limits.thy file | annotate | diff | revisions src/HOL/SEQ.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Library/Topology_Euclidean_Space.thy	Fri Jun 05 15:59:20 2009 -0700
1.2 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Sat Jun 06 09:11:12 2009 -0700
1.3 @@ -1171,46 +1171,50 @@
1.4  subsection{* Limits, defined as vacuously true when the limit is trivial. *}
1.5
1.6    text{* Notation Lim to avoid collition with lim defined in analysis *}
1.7 -definition "Lim net f = (THE l. (f ---> l) net)"
1.8 +definition
1.9 +  Lim :: "'a net \<Rightarrow> ('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'b" where
1.10 +  "Lim net f = (THE l. (f ---> l) net)"
1.11
1.12  lemma Lim:
1.13   "(f ---> l) net \<longleftrightarrow>
1.14          trivial_limit net \<or>
1.15          (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
1.16 -  unfolding tendsto_def trivial_limit_eq by auto
1.17 +  unfolding tendsto_iff trivial_limit_eq by auto
1.18
1.19
1.20  text{* Show that they yield usual definitions in the various cases. *}
1.21
1.22  lemma Lim_within_le: "(f ---> l)(at a within S) \<longleftrightarrow>
1.23             (\<forall>e>0. \<exists>d>0. \<forall>x\<in>S. 0 < dist x a  \<and> dist x a  <= d \<longrightarrow> dist (f x) l < e)"
1.24 -  by (auto simp add: tendsto_def eventually_within_le)
1.25 +  by (auto simp add: tendsto_iff eventually_within_le)
1.26
1.27  lemma Lim_within: "(f ---> l) (at a within S) \<longleftrightarrow>
1.28          (\<forall>e >0. \<exists>d>0. \<forall>x \<in> S. 0 < dist x a  \<and> dist x a  < d  \<longrightarrow> dist (f x) l < e)"
1.29 -  by (auto simp add: tendsto_def eventually_within)
1.30 +  by (auto simp add: tendsto_iff eventually_within)
1.31
1.32  lemma Lim_at: "(f ---> l) (at a) \<longleftrightarrow>
1.33          (\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a  \<and> dist x a  < d  \<longrightarrow> dist (f x) l < e)"
1.34 -  by (auto simp add: tendsto_def eventually_at)
1.35 +  by (auto simp add: tendsto_iff eventually_at)
1.36
1.37  lemma Lim_at_iff_LIM: "(f ---> l) (at a) \<longleftrightarrow> f -- a --> l"
1.38    unfolding Lim_at LIM_def by (simp only: zero_less_dist_iff)
1.39
1.40  lemma Lim_at_infinity:
1.41    "(f ---> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x::real^'n::finite. norm x >= b \<longrightarrow> dist (f x) l < e)"
1.42 -  by (auto simp add: tendsto_def eventually_at_infinity)
1.43 +  by (auto simp add: tendsto_iff eventually_at_infinity)
1.44
1.45  lemma Lim_sequentially:
1.46   "(S ---> l) sequentially \<longleftrightarrow>
1.47            (\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (S n) l < e)"
1.48 -  by (auto simp add: tendsto_def eventually_sequentially)
1.49 +  by (auto simp add: tendsto_iff eventually_sequentially)
1.50
1.51  lemma Lim_sequentially_iff_LIMSEQ: "(S ---> l) sequentially \<longleftrightarrow> S ----> l"
1.52    unfolding Lim_sequentially LIMSEQ_def ..
1.53
1.54 -lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f ---> l) net"
1.55 -  unfolding tendsto_def by (auto elim: eventually_rev_mono)
1.56 +lemma Lim_eventually:
1.57 +  fixes l :: "'a::metric_space" (* FIXME: generalize to t2_space *)
1.58 +  shows "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f ---> l) net"
1.59 +  unfolding tendsto_iff by (auto elim: eventually_rev_mono)
1.60
1.61  text{* The expected monotonicity property. *}
1.62
1.63 @@ -1225,7 +1229,7 @@
1.64    shows "(f ---> l) (net within (S \<union> T))"
1.65    using assms unfolding tendsto_def Limits.eventually_within
1.66    apply clarify
1.67 -  apply (drule spec, drule (1) mp)+
1.68 +  apply (drule (1) bspec)+
1.69    apply (auto elim: eventually_elim2)
1.70    done
1.71
1.72 @@ -1238,9 +1242,11 @@
1.73
1.74  lemma Lim_at_within: "(f ---> l) net ==> (f ---> l)(net within S)"
1.75    unfolding tendsto_def Limits.eventually_within
1.76 +  apply (clarify, drule (1) bspec)
1.77    by (auto elim!: eventually_elim1)
1.78
1.79  lemma Lim_within_open:
1.80 +  fixes l :: "'a::metric_space" (* FIXME: generalize to topological_space *)
1.81    assumes"a \<in> S" "open S"
1.82    shows "(f ---> l)(at a within S) \<longleftrightarrow> (f ---> l)(at a)" (is "?lhs \<longleftrightarrow> ?rhs")
1.83  proof
1.84 @@ -1268,7 +1274,9 @@
1.85  text{* Another limit point characterization. *}
1.86
1.87  lemma islimpt_sequential:
1.88 - "x islimpt S \<longleftrightarrow> (\<exists>f. (\<forall>n::nat. f n \<in> S -{x}) \<and> (f ---> x) sequentially)" (is "?lhs = ?rhs")
1.89 +  fixes x :: "'a::metric_space" (* FIXME: generalize to topological_space *)
1.90 +  shows "x islimpt S \<longleftrightarrow> (\<exists>f. (\<forall>n::nat. f n \<in> S -{x}) \<and> (f ---> x) sequentially)"
1.91 +    (is "?lhs = ?rhs")
1.92  proof
1.93    assume ?lhs
1.94    then obtain f where f:"\<forall>y. y>0 \<longrightarrow> f y \<in> S \<and> f y \<noteq> x \<and> dist (f y) x < y"
1.95 @@ -1317,11 +1325,11 @@
1.96        apply (simp add: pos_less_divide_eq `0 < b` mult_commute)
1.97        done
1.98    }
1.99 -  thus ?thesis unfolding tendsto_def by simp
1.100 +  thus ?thesis unfolding tendsto_iff by simp
1.101  qed
1.102
1.103  lemma Lim_const: "((\<lambda>x. a) ---> a) net"
1.104 -  by (auto simp add: Lim trivial_limit_def)
1.105 +  unfolding tendsto_def by simp
1.106
1.107  lemma Lim_cmul:
1.108    fixes f :: "'a \<Rightarrow> real ^ 'n::finite"
1.109 @@ -1355,7 +1363,7 @@
1.110        apply simp
1.111        done
1.112    }
1.113 -  thus ?thesis unfolding tendsto_def by simp
1.114 +  thus ?thesis unfolding tendsto_iff by simp
1.115  qed
1.116
1.117  lemma Lim_sub:
1.118 @@ -1377,7 +1385,7 @@
1.119    fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
1.120    assumes "eventually (\<lambda>x. norm(f x) <= g x) net" "((\<lambda>x. vec1(g x)) ---> 0) net"
1.121    shows "(f ---> 0) net"
1.124    fix e::real assume "0<e"
1.125    { fix x
1.126      assume "norm (f x) \<le> g x" "dist (vec1 (g x)) 0 < e"
1.127 @@ -1387,12 +1395,12 @@
1.128    thus "eventually (\<lambda>x. dist (f x) 0 < e) net"
1.129      using eventually_and[of "\<lambda>x. norm(f x) <= g x" "\<lambda>x. dist (vec1 (g x)) 0 < e" net]
1.130      using eventually_mono[of "(\<lambda>x. norm (f x) \<le> g x \<and> dist (vec1 (g x)) 0 < e)" "(\<lambda>x. dist (f x) 0 < e)" net]
1.131 -    using assms `e>0` unfolding tendsto_def by auto
1.132 +    using assms `e>0` unfolding tendsto_iff by auto
1.133  qed
1.134
1.135  lemma Lim_component: "(f ---> l) net
1.136                        ==> ((\<lambda>a. vec1((f a :: real ^'n::finite)\$i)) ---> vec1(l\$i)) net"
1.137 -  unfolding tendsto_def
1.138 +  unfolding tendsto_iff
1.139    apply (simp add: dist_norm vec1_sub[symmetric] norm_vec1  vector_minus_component[symmetric] del: vector_minus_component)
1.140    apply (auto simp del: vector_minus_component)
1.141    apply (erule_tac x=e in allE)
1.142 @@ -1408,7 +1416,7 @@
1.143    fixes g :: "'a \<Rightarrow> 'c::real_normed_vector"
1.144    assumes "eventually (\<lambda>n. norm(f n) <= norm(g n)) net"  "(g ---> 0) net"
1.145    shows "(f ---> 0) net"
1.148    fix e::real assume "e>0"
1.149    { fix x
1.150      assume "norm (f x) \<le> norm (g x)" "dist (g x) 0 < e"
1.151 @@ -1416,12 +1424,13 @@
1.152    thus "eventually (\<lambda>x. dist (f x) 0 < e) net"
1.153      using eventually_and[of "\<lambda>x. norm (f x) \<le> norm (g x)" "\<lambda>x. dist (g x) 0 < e" net]
1.154      using eventually_mono[of "\<lambda>x. norm (f x) \<le> norm (g x) \<and> dist (g x) 0 < e" "\<lambda>x. dist (f x) 0 < e" net]
1.155 -    using assms `e>0` unfolding tendsto_def by blast
1.156 +    using assms `e>0` unfolding tendsto_iff by blast
1.157  qed
1.158
1.159  text{* Deducing things about the limit from the elements. *}
1.160
1.161  lemma Lim_in_closed_set:
1.162 +  fixes l :: "'a::metric_space" (* FIXME: generalize to topological_space *)
1.163    assumes "closed S" "eventually (\<lambda>x. f(x) \<in> S) net"  "\<not>(trivial_limit net)" "(f ---> l) net"
1.164    shows "l \<in> S"
1.165  proof (rule ccontr)
1.166 @@ -1581,17 +1590,21 @@
1.167        by (auto elim: eventually_rev_mono)
1.168    }
1.169    thus "((\<lambda>x. h (f x) (g x)) ---> h l m) net"
1.170 -    unfolding tendsto_def by simp
1.171 +    unfolding tendsto_iff by simp
1.172  qed
1.173
1.174  text{* These are special for limits out of the same vector space. *}
1.175
1.176 -lemma Lim_within_id: "(id ---> a) (at a within s)" by (auto simp add: Lim_within id_def)
1.177 +lemma Lim_within_id: "(id ---> a) (at a within s)"
1.178 +  unfolding tendsto_def Limits.eventually_within eventually_at_topological
1.179 +  by auto
1.180 +
1.181  lemma Lim_at_id: "(id ---> a) (at a)"
1.182  apply (subst within_UNIV[symmetric]) by (simp add: Lim_within_id)
1.183
1.184  lemma Lim_at_zero:
1.185    fixes a :: "'a::real_normed_vector"
1.186 +  fixes l :: "'b::metric_space" (* FIXME: generalize to topological_space *)
1.187    shows "(f ---> l) (at a) \<longleftrightarrow> ((\<lambda>x. f(a + x)) ---> l) (at 0)" (is "?lhs = ?rhs")
1.188  proof
1.189    assume "?lhs"
1.190 @@ -1671,13 +1684,15 @@
1.191  qed
1.192
1.193  lemma Lim_transform_eventually:
1.194 +  fixes l :: "'a::metric_space" (* FIXME: generalize to t2_space *)
1.195    shows "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f ---> l) net ==> (g ---> l) net"
1.196 -  unfolding tendsto_def
1.197 +  unfolding tendsto_iff
1.198    apply (clarify, drule spec, drule (1) mp)
1.199    apply (erule (1) eventually_elim2, simp)
1.200    done
1.201
1.202  lemma Lim_transform_within:
1.203 +  fixes l :: "'b::metric_space" (* TODO: generalize *)
1.204    assumes "0 < d" "(\<forall>x'\<in>S. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x')"
1.205            "(f ---> l) (at x within S)"
1.206    shows   "(g ---> l) (at x within S)"
1.207 @@ -1691,6 +1706,7 @@
1.208    done
1.209
1.210  lemma Lim_transform_at:
1.211 +  fixes l :: "'b::metric_space" (* TODO: generalize *)
1.212    shows "0 < d \<Longrightarrow> (\<forall>x'. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x') \<Longrightarrow>
1.213    (f ---> l) (at x) ==> (g ---> l) (at x)"
1.214    apply (subst within_UNIV[symmetric])
1.215 @@ -1701,6 +1717,7 @@
1.216
1.217  lemma Lim_transform_away_within:
1.218    fixes a b :: "'a::metric_space"
1.219 +  fixes l :: "'b::metric_space" (* TODO: generalize *)
1.220    assumes "a\<noteq>b" "\<forall>x\<in> S. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
1.221    and "(f ---> l) (at a within S)"
1.222    shows "(g ---> l) (at a within S)"
1.223 @@ -1712,6 +1729,7 @@
1.224
1.225  lemma Lim_transform_away_at:
1.226    fixes a b :: "'a::metric_space"
1.227 +  fixes l :: "'b::metric_space" (* TODO: generalize *)
1.228    assumes ab: "a\<noteq>b" and fg: "\<forall>x. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
1.229    and fl: "(f ---> l) (at a)"
1.230    shows "(g ---> l) (at a)"
1.231 @@ -1722,6 +1740,7 @@
1.232
1.233  lemma Lim_transform_within_open:
1.234    fixes a :: "'a::metric_space"
1.235 +  fixes l :: "'b::metric_space" (* TODO: generalize *)
1.236    assumes "open S"  "a \<in> S"  "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> f x = g x"  "(f ---> l) (at a)"
1.237    shows "(g ---> l) (at a)"
1.238  proof-
1.239 @@ -1736,19 +1755,22 @@
1.240  (* FIXME: Only one congruence rule for tendsto can be used at a time! *)
1.241
1.243 -  fixes a :: "'a::metric_space" shows
1.244 - "(\<And>x. x \<noteq> a \<Longrightarrow> f x = g x) ==> ((\<lambda>x. f x) ---> l) (at a within S) \<longleftrightarrow> ((g ---> l) (at a within S))"
1.245 +  fixes a :: "'a::metric_space"
1.246 +  fixes l :: "'b::metric_space" (* TODO: generalize *)
1.247 +  shows "(\<And>x. x \<noteq> a \<Longrightarrow> f x = g x) ==> ((\<lambda>x. f x) ---> l) (at a within S) \<longleftrightarrow> ((g ---> l) (at a within S))"
1.248    by (simp add: Lim_within dist_nz[symmetric])
1.249
1.251 -  fixes a :: "'a::metric_space" shows
1.252 - "(\<And>x. x \<noteq> a ==> f x = g x) ==> (((\<lambda>x. f x) ---> l) (at a) \<longleftrightarrow> ((g ---> l) (at a)))"
1.253 +  fixes a :: "'a::metric_space"
1.254 +  fixes l :: "'b::metric_space" (* TODO: generalize *)
1.255 +  shows "(\<And>x. x \<noteq> a ==> f x = g x) ==> (((\<lambda>x. f x) ---> l) (at a) \<longleftrightarrow> ((g ---> l) (at a)))"
1.256    by (simp add: Lim_at dist_nz[symmetric])
1.257
1.258  text{* Useful lemmas on closure and set of possible sequential limits.*}
1.259
1.260  lemma closure_sequential:
1.261 - "l \<in> closure S \<longleftrightarrow> (\<exists>x. (\<forall>n. x n \<in> S) \<and> (x ---> l) sequentially)" (is "?lhs = ?rhs")
1.262 +  fixes l :: "'a::metric_space" (* TODO: generalize *)
1.263 +  shows "l \<in> closure S \<longleftrightarrow> (\<exists>x. (\<forall>n. x n \<in> S) \<and> (x ---> l) sequentially)" (is "?lhs = ?rhs")
1.264  proof
1.265    assume "?lhs" moreover
1.266    { assume "l \<in> S"
1.267 @@ -1783,17 +1805,23 @@
1.268
1.269  text{* Some other lemmas about sequences. *}
1.270
1.271 -lemma seq_offset: "(f ---> l) sequentially ==> ((\<lambda>i. f( i + k)) ---> l) sequentially"
1.272 +lemma seq_offset:
1.273 +  fixes l :: "'a::metric_space" (* TODO: generalize *)
1.274 +  shows "(f ---> l) sequentially ==> ((\<lambda>i. f( i + k)) ---> l) sequentially"
1.275    apply (auto simp add: Lim_sequentially)
1.277
1.278 -lemma seq_offset_neg: "(f ---> l) sequentially ==> ((\<lambda>i. f(i - k)) ---> l) sequentially"
1.279 +lemma seq_offset_neg:
1.280 +  fixes l :: "'a::metric_space" (* TODO: generalize *)
1.281 +  shows "(f ---> l) sequentially ==> ((\<lambda>i. f(i - k)) ---> l) sequentially"
1.283    apply (subgoal_tac "\<And>N k (n::nat). N + k <= n ==> N <= n - k")
1.284    apply metis
1.285    by arith
1.286
1.287 -lemma seq_offset_rev: "((\<lambda>i. f(i + k)) ---> l) sequentially ==> (f ---> l) sequentially"
1.288 +lemma seq_offset_rev:
1.289 +  fixes l :: "'a::metric_space" (* TODO: generalize *)
1.290 +  shows "((\<lambda>i. f(i + k)) ---> l) sequentially ==> (f ---> l) sequentially"
1.292    apply (subgoal_tac "\<And>N k (n::nat). N + k <= n ==> N <= n - k \<and> (n - k) + k = n")
1.293    by metis arith
1.294 @@ -2017,8 +2045,9 @@
1.295
1.296  lemma lim_within_interior:
1.297    fixes x :: "'a::metric_space"
1.298 +  fixes l :: "'b::metric_space" (* TODO: generalize *)
1.299    shows "x \<in> interior S  ==> ((f ---> l) (at x within S) \<longleftrightarrow> (f ---> l) (at x))"
1.300 -  by (simp add: tendsto_def eventually_within_interior)
1.301 +  by (simp add: tendsto_iff eventually_within_interior)
1.302
1.303  lemma netlimit_within_interior:
1.304    fixes x :: "'a::{perfect_space, real_normed_vector}"
1.305 @@ -2241,7 +2270,9 @@
1.306
1.307  subsection{* Compactness (the definition is the one based on convegent subsequences). *}
1.308
1.309 -definition "compact S \<longleftrightarrow>
1.310 +definition
1.311 +  compact :: "'a::metric_space set \<Rightarrow> bool" where (* TODO: generalize *)
1.312 +  "compact S \<longleftrightarrow>
1.313     (\<forall>f. (\<forall>n::nat. f n \<in> S) \<longrightarrow>
1.314         (\<exists>l\<in>S. \<exists>r. (\<forall>m n. m < n \<longrightarrow> r m < r n) \<and> ((f o r) ---> l) sequentially))"
1.315
1.316 @@ -2256,7 +2287,9 @@
1.317    ultimately show "Suc n \<le> r (Suc n)" by auto
1.318  qed
1.319
1.320 -lemma lim_subsequence: "\<forall>m n. m < n \<longrightarrow> r m < r n \<Longrightarrow> (s ---> l) sequentially \<Longrightarrow> ((s o r) ---> l) sequentially"
1.321 +lemma lim_subsequence:
1.322 +  fixes l :: "'a::metric_space" (* TODO: generalize *)
1.323 +  shows "\<forall>m n. m < n \<longrightarrow> r m < r n \<Longrightarrow> (s ---> l) sequentially \<Longrightarrow> ((s o r) ---> l) sequentially"
1.324  unfolding Lim_sequentially by (simp, metis  monotone_bigger le_trans)
1.325
1.326  lemma num_Axiom: "EX! g. g 0 = e \<and> (\<forall>n. g (Suc n) = f n (g n))"
1.327 @@ -2700,6 +2733,7 @@
1.328  qed
1.329
1.330  lemma sequence_infinite_lemma:
1.331 +  fixes l :: "'a::metric_space" (* TODO: generalize *)
1.332    assumes "\<forall>n::nat. (f n  \<noteq> l)"  "(f ---> l) sequentially"
1.333    shows "infinite {y. (\<exists> n. y = f n)}"
1.334  proof(rule ccontr)
1.335 @@ -2714,6 +2748,7 @@
1.336  qed
1.337
1.338  lemma sequence_unique_limpt:
1.339 +  fixes l :: "'a::metric_space" (* TODO: generalize *)
1.340    assumes "\<forall>n::nat. (f n \<noteq> l)"  "(f ---> l) sequentially"  "l' islimpt {y.  (\<exists>n. y = f n)}"
1.341    shows "l' = l"
1.342  proof(rule ccontr)
1.343 @@ -3049,15 +3084,18 @@
1.344
1.345  subsection{* Define continuity over a net to take in restrictions of the set. *}
1.346
1.347 -definition "continuous net f \<longleftrightarrow> (f ---> f(netlimit net)) net"
1.348 +definition
1.349 +  continuous :: "'a::metric_space net \<Rightarrow> ('a \<Rightarrow> 'b::metric_space) \<Rightarrow> bool" where
1.350 +  "continuous net f \<longleftrightarrow> (f ---> f(netlimit net)) net"
1.351 +  (* FIXME: generalize 'b to topological_space *)
1.352
1.353  lemma continuous_trivial_limit:
1.354   "trivial_limit net ==> continuous net f"
1.355 -  unfolding continuous_def tendsto_def trivial_limit_eq by auto
1.356 +  unfolding continuous_def tendsto_iff trivial_limit_eq by auto
1.357
1.358  lemma continuous_within: "continuous (at x within s) f \<longleftrightarrow> (f ---> f(x)) (at x within s)"
1.359    unfolding continuous_def
1.360 -  unfolding tendsto_def
1.361 +  unfolding tendsto_iff
1.362    using netlimit_within[of x s]
1.363    by (cases "trivial_limit (at x within s)") (auto simp add: trivial_limit_eventually)
1.364
1.365 @@ -3149,7 +3187,7 @@
1.366    shows "continuous_on s f"
1.367  proof(simp add: continuous_at continuous_on_def, rule, rule, rule)
1.368    fix x and e::real assume "x\<in>s" "e>0"
1.369 -  hence "eventually (\<lambda>xa. dist (f xa) (f x) < e) (at x)" using assms unfolding continuous_at tendsto_def by auto
1.370 +  hence "eventually (\<lambda>xa. dist (f xa) (f x) < e) (at x)" using assms unfolding continuous_at tendsto_iff by auto
1.371    then obtain d where d:"d>0" "\<forall>xa. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (f x) < e" unfolding eventually_at by auto
1.372    { fix x' assume "\<not> 0 < dist x' x"
1.373      hence "x=x'"
1.374 @@ -4025,7 +4063,7 @@
1.375  proof-
1.376    { fix e::real and x assume "0 < dist x a" "dist x a < e" "e>0"
1.377      hence "\<bar>x \$ i - a \$ i\<bar> < e" using component_le_norm[of "x - a" i] unfolding dist_norm by auto  }
1.378 -  thus ?thesis unfolding continuous_at tendsto_def eventually_at dist_vec1 by auto
1.379 +  thus ?thesis unfolding continuous_at tendsto_iff eventually_at dist_vec1 by auto
1.380  qed
1.381
1.382  lemma continuous_on_vec1_component:
1.383 @@ -4207,7 +4245,7 @@
1.384      have "eventually (\<lambda>x. dist ((vec1 o inverse o f) x) (vec1(inverse l)) < e) net"
1.385        by (auto elim: eventually_rev_mono)
1.386    }
1.387 -  thus ?thesis unfolding tendsto_def by auto
1.388 +  thus ?thesis unfolding tendsto_iff by auto
1.389  qed
1.390
1.391  lemma continuous_inv:
1.392 @@ -5058,7 +5096,7 @@
1.393      ultimately have "eventually (\<lambda>x. \<bar>a \<bullet> f x - a \<bullet> l\<bar> < e) net"
1.394        by (auto elim: eventually_rev_mono)
1.395    }
1.396 -  thus ?thesis unfolding tendsto_def
1.397 +  thus ?thesis unfolding tendsto_iff
1.398      by (auto simp add: dist_vec1)
1.399  qed
1.400
1.401 @@ -5166,11 +5204,17 @@
1.402
1.403  text{* Limits relative to a union.                                               *}
1.404
1.405 +lemma eventually_within_Un:
1.406 +  "eventually P (net within (s \<union> t)) \<longleftrightarrow>
1.407 +    eventually P (net within s) \<and> eventually P (net within t)"
1.408 +  unfolding Limits.eventually_within
1.409 +  by (auto elim!: eventually_rev_mp)
1.410 +
1.411  lemma Lim_within_union:
1.412   "(f ---> l) (net within (s \<union> t)) \<longleftrightarrow>
1.413    (f ---> l) (net within s) \<and> (f ---> l) (net within t)"
1.414 -  unfolding tendsto_def Limits.eventually_within
1.415 -  by (auto elim!: eventually_elim1 intro: eventually_conjI)
1.416 +  unfolding tendsto_def
1.417 +  by (auto simp add: eventually_within_Un)
1.418
1.419  lemma continuous_on_union:
1.420    assumes "closed s" "closed t" "continuous_on s f" "continuous_on t f"
```
```     2.1 --- a/src/HOL/Lim.thy	Fri Jun 05 15:59:20 2009 -0700
2.2 +++ b/src/HOL/Lim.thy	Sat Jun 06 09:11:12 2009 -0700
2.3 @@ -30,7 +30,7 @@
2.4  subsection {* Limits of Functions *}
2.5
2.6  lemma LIM_conv_tendsto: "(f -- a --> L) \<longleftrightarrow> (f ---> L) (at a)"
2.7 -unfolding LIM_def tendsto_def eventually_at ..
2.8 +unfolding LIM_def tendsto_iff eventually_at ..
2.9
2.10  lemma metric_LIM_I:
2.11    "(\<And>r. 0 < r \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r)
```
```     3.1 --- a/src/HOL/Limits.thy	Fri Jun 05 15:59:20 2009 -0700
3.2 +++ b/src/HOL/Limits.thy	Sat Jun 06 09:11:12 2009 -0700
3.3 @@ -353,21 +353,47 @@
3.4  subsection{* Limits *}
3.5
3.6  definition
3.7 -  tendsto :: "('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'b \<Rightarrow> 'a net \<Rightarrow> bool"
3.8 -    (infixr "--->" 55) where
3.9 -  [code del]: "(f ---> l) net \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
3.10 +  tendsto :: "('a \<Rightarrow> 'b::topological_space) \<Rightarrow> 'b \<Rightarrow> 'a net \<Rightarrow> bool"
3.11 +    (infixr "--->" 55)
3.12 +where [code del]:
3.13 +  "(f ---> l) net \<longleftrightarrow> (\<forall>S\<in>topo. l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)"
3.14
3.15 -lemma tendstoI:
3.16 -  "(\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net)
3.17 +lemma topological_tendstoI:
3.18 +  "(\<And>S. S \<in> topo \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) net)
3.19      \<Longrightarrow> (f ---> l) net"
3.20    unfolding tendsto_def by auto
3.21
3.22 +lemma topological_tendstoD:
3.23 +  "(f ---> l) net \<Longrightarrow> S \<in> topo \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) net"
3.24 +  unfolding tendsto_def by auto
3.25 +
3.26 +lemma tendstoI:
3.27 +  assumes "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net"
3.28 +  shows "(f ---> l) net"
3.29 +apply (rule topological_tendstoI)
3.31 +apply (drule (1) bspec, clarify)
3.32 +apply (drule assms)
3.33 +apply (erule eventually_elim1, simp)
3.34 +done
3.35 +
3.36  lemma tendstoD:
3.37    "(f ---> l) net \<Longrightarrow> 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net"
3.38 -  unfolding tendsto_def by auto
3.39 +apply (drule_tac S="{x. dist x l < e}" in topological_tendstoD)
3.40 +apply (clarsimp simp add: topo_dist)
3.41 +apply (rule_tac x="e - dist x l" in exI, clarsimp)
3.42 +apply (simp only: less_diff_eq)
3.43 +apply (erule le_less_trans [OF dist_triangle])
3.44 +apply simp
3.45 +apply simp
3.46 +done
3.47 +
3.48 +lemma tendsto_iff:
3.49 +  "(f ---> l) net \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
3.50 +using tendstoI tendstoD by fast
3.51
3.52  lemma tendsto_Zfun_iff: "(f ---> a) net = Zfun (\<lambda>x. f x - a) net"
3.53 -by (simp only: tendsto_def Zfun_def dist_norm)
3.54 +by (simp only: tendsto_iff Zfun_def dist_norm)
3.55
3.56  lemma tendsto_const: "((\<lambda>x. k) ---> k) net"
3.58 @@ -375,7 +401,7 @@
3.59  lemma tendsto_norm:
3.60    fixes a :: "'a::real_normed_vector"
3.61    shows "(f ---> a) net \<Longrightarrow> ((\<lambda>x. norm (f x)) ---> norm a) net"
3.62 -apply (simp add: tendsto_def dist_norm, safe)
3.63 +apply (simp add: tendsto_iff dist_norm, safe)
3.64  apply (drule_tac x="e" in spec, safe)
3.65  apply (erule eventually_elim1)
3.66  apply (erule order_le_less_trans [OF norm_triangle_ineq3])
```
```     4.1 --- a/src/HOL/SEQ.thy	Fri Jun 05 15:59:20 2009 -0700
4.2 +++ b/src/HOL/SEQ.thy	Sat Jun 06 09:11:12 2009 -0700
4.3 @@ -194,7 +194,7 @@
4.4  subsection {* Limits of Sequences *}
4.5
4.6  lemma LIMSEQ_conv_tendsto: "(X ----> L) \<longleftrightarrow> (X ---> L) sequentially"
4.7 -unfolding LIMSEQ_def tendsto_def eventually_sequentially ..
4.8 +unfolding LIMSEQ_def tendsto_iff eventually_sequentially ..
4.9
4.10  lemma LIMSEQ_iff:
4.11    fixes L :: "'a::real_normed_vector"
```