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])