src/HOL/Limits.thy
 changeset 31488 5691ccb8d6b5 parent 31487 93938cafc0e6 child 31492 5400beeddb55
```     1.1 --- a/src/HOL/Limits.thy	Fri Jun 05 15:59:20 2009 -0700
1.2 +++ b/src/HOL/Limits.thy	Sat Jun 06 09:11:12 2009 -0700
1.3 @@ -353,21 +353,47 @@
1.4  subsection{* Limits *}
1.5
1.6  definition
1.7 -  tendsto :: "('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'b \<Rightarrow> 'a net \<Rightarrow> bool"
1.8 -    (infixr "--->" 55) where
1.9 -  [code del]: "(f ---> l) net \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
1.10 +  tendsto :: "('a \<Rightarrow> 'b::topological_space) \<Rightarrow> 'b \<Rightarrow> 'a net \<Rightarrow> bool"
1.11 +    (infixr "--->" 55)
1.12 +where [code del]:
1.13 +  "(f ---> l) net \<longleftrightarrow> (\<forall>S\<in>topo. l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)"
1.14
1.15 -lemma tendstoI:
1.16 -  "(\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net)
1.17 +lemma topological_tendstoI:
1.18 +  "(\<And>S. S \<in> topo \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) net)
1.19      \<Longrightarrow> (f ---> l) net"
1.20    unfolding tendsto_def by auto
1.21
1.22 +lemma topological_tendstoD:
1.23 +  "(f ---> l) net \<Longrightarrow> S \<in> topo \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) net"
1.24 +  unfolding tendsto_def by auto
1.25 +
1.26 +lemma tendstoI:
1.27 +  assumes "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net"
1.28 +  shows "(f ---> l) net"
1.29 +apply (rule topological_tendstoI)
1.30 +apply (simp add: topo_dist)
1.31 +apply (drule (1) bspec, clarify)
1.32 +apply (drule assms)
1.33 +apply (erule eventually_elim1, simp)
1.34 +done
1.35 +
1.36  lemma tendstoD:
1.37    "(f ---> l) net \<Longrightarrow> 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net"
1.38 -  unfolding tendsto_def by auto
1.39 +apply (drule_tac S="{x. dist x l < e}" in topological_tendstoD)
1.40 +apply (clarsimp simp add: topo_dist)
1.41 +apply (rule_tac x="e - dist x l" in exI, clarsimp)
1.42 +apply (simp only: less_diff_eq)
1.43 +apply (erule le_less_trans [OF dist_triangle])
1.44 +apply simp
1.45 +apply simp
1.46 +done
1.47 +
1.48 +lemma tendsto_iff:
1.49 +  "(f ---> l) net \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
1.50 +using tendstoI tendstoD by fast
1.51
1.52  lemma tendsto_Zfun_iff: "(f ---> a) net = Zfun (\<lambda>x. f x - a) net"
1.53 -by (simp only: tendsto_def Zfun_def dist_norm)
1.54 +by (simp only: tendsto_iff Zfun_def dist_norm)
1.55
1.56  lemma tendsto_const: "((\<lambda>x. k) ---> k) net"
1.57  by (simp add: tendsto_def)
1.58 @@ -375,7 +401,7 @@
1.59  lemma tendsto_norm:
1.60    fixes a :: "'a::real_normed_vector"
1.61    shows "(f ---> a) net \<Longrightarrow> ((\<lambda>x. norm (f x)) ---> norm a) net"
1.62 -apply (simp add: tendsto_def dist_norm, safe)
1.63 +apply (simp add: tendsto_iff dist_norm, safe)
1.64  apply (drule_tac x="e" in spec, safe)
1.65  apply (erule eventually_elim1)
1.66  apply (erule order_le_less_trans [OF norm_triangle_ineq3])
```