# HG changeset patch
# User huffman
# Date 1314374189 25200
# Node ID 7abe4a59f75d1f50c8652211f4193ccfc82468af
# Parent  a2e9b39df93874d2a752d1300642eb17a1ff4d1a
generalize and simplify proof of continuous_within_sequentially

diff -r a2e9b39df938 -r 7abe4a59f75d src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Aug 26 08:12:38 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Aug 26 08:56:29 2011 -0700
@@ -3309,56 +3309,41 @@
 
 text {* Characterization of various kinds of continuity in terms of sequences. *}
 
-(* \<longrightarrow> could be generalized, but \<longleftarrow> requires metric space *)
 lemma continuous_within_sequentially:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
   shows "continuous (at a within s) f \<longleftrightarrow>
                 (\<forall>x. (\<forall>n::nat. x n \<in> s) \<and> (x ---> a) sequentially
                      --> ((f o x) ---> f a) sequentially)" (is "?lhs = ?rhs")
 proof
   assume ?lhs
-  { fix x::"nat \<Rightarrow> 'a" assume x:"\<forall>n. x n \<in> s" "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (x n) a < e"
-    fix e::real assume "e>0"
-    from `?lhs` obtain d where "d>0" and d:"\<forall>x\<in>s. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) (f a) < e" unfolding continuous_within Lim_within using `e>0` by auto
-    from x(2) `d>0` obtain N where N:"\<forall>n\<ge>N. dist (x n) a < d" by auto
-    hence "\<exists>N. \<forall>n\<ge>N. dist ((f \<circ> x) n) (f a) < e"
-      apply(rule_tac  x=N in exI) using N d  apply auto using x(1)
-      apply(erule_tac x=n in allE) apply(erule_tac x=n in allE)
-      apply(erule_tac x="x n" in ballE)  apply auto unfolding dist_nz[THEN sym] apply auto using `e>0` by auto
+  { fix x::"nat \<Rightarrow> 'a" assume x:"\<forall>n. x n \<in> s" "\<forall>e>0. eventually (\<lambda>n. dist (x n) a < e) sequentially"
+    fix T::"'b set" assume "open T" and "f a \<in> T"
+    with `?lhs` obtain d where "d>0" and d:"\<forall>x\<in>s. 0 < dist x a \<and> dist x a < d \<longrightarrow> f x \<in> T"
+      unfolding continuous_within tendsto_def eventually_within by auto
+    have "eventually (\<lambda>n. dist (x n) a < d) sequentially"
+      using x(2) `d>0` by simp
+    hence "eventually (\<lambda>n. (f \<circ> x) n \<in> T) sequentially"
+    proof (rule eventually_elim1)
+      fix n assume "dist (x n) a < d" thus "(f \<circ> x) n \<in> T"
+        using d x(1) `f a \<in> T` unfolding dist_nz[THEN sym] by auto
+    qed
   }
-  thus ?rhs unfolding continuous_within unfolding Lim_sequentially by simp
+  thus ?rhs unfolding tendsto_iff unfolding tendsto_def by simp
 next
-  assume ?rhs
-  { fix e::real assume "e>0"
-    assume "\<not> (\<exists>d>0. \<forall>x\<in>s. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) (f a) < e)"
-    hence "\<forall>d. \<exists>x. d>0 \<longrightarrow> x\<in>s \<and> (0 < dist x a \<and> dist x a < d \<and> \<not> dist (f x) (f a) < e)" by blast
-    then obtain x where x:"\<forall>d>0. x d \<in> s \<and> (0 < dist (x d) a \<and> dist (x d) a < d \<and> \<not> dist (f (x d)) (f a) < e)"
-      using choice[of "\<lambda>d x.0<d \<longrightarrow> x\<in>s \<and> (0 < dist x a \<and> dist x a < d \<and> \<not> dist (f x) (f a) < e)"] by auto
-    { fix d::real assume "d>0"
-      hence "\<exists>N::nat. inverse (real (N + 1)) < d" using real_arch_inv[of d] by (auto, rule_tac x="n - 1" in exI)auto
-      then obtain N::nat where N:"inverse (real (N + 1)) < d" by auto
-      { fix n::nat assume n:"n\<ge>N"
-        hence "dist (x (inverse (real (n + 1)))) a < inverse (real (n + 1))" using x[THEN spec[where x="inverse (real (n + 1))"]] by auto
-        moreover have "inverse (real (n + 1)) < d" using N n by (auto, metis Suc_le_mono le_SucE less_imp_inverse_less nat_le_real_less order_less_trans real_of_nat_Suc real_of_nat_Suc_gt_zero)
-        ultimately have "dist (x (inverse (real (n + 1)))) a < d" by auto
-      }
-      hence "\<exists>N::nat. \<forall>n\<ge>N. dist (x (inverse (real (n + 1)))) a < d" by auto
-    }
-    hence "(\<forall>n::nat. x (inverse (real (n + 1))) \<in> s) \<and> (\<forall>e>0. \<exists>N::nat. \<forall>n\<ge>N. dist (x (inverse (real (n + 1)))) a < e)" using x by auto
-    hence "\<forall>e>0. \<exists>N::nat. \<forall>n\<ge>N. dist (f (x (inverse (real (n + 1))))) (f a) < e"  using `?rhs`[THEN spec[where x="\<lambda>n::nat. x (inverse (real (n+1)))"], unfolded Lim_sequentially] by auto
-    hence "False" apply(erule_tac x=e in allE) using `e>0` using x by auto
-  }
-  thus ?lhs  unfolding continuous_within unfolding Lim_within unfolding Lim_sequentially by blast
+  assume ?rhs thus ?lhs
+    unfolding continuous_within tendsto_def [where l="f a"]
+    by (simp add: sequentially_imp_eventually_within)
 qed
 
 lemma continuous_at_sequentially:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
   shows "continuous (at a) f \<longleftrightarrow> (\<forall>x. (x ---> a) sequentially
                   --> ((f o x) ---> f a) sequentially)"
-  using continuous_within_sequentially[of a UNIV f] unfolding within_UNIV by auto
+  using continuous_within_sequentially[of a UNIV f]
+  unfolding within_UNIV by auto
 
 lemma continuous_on_sequentially:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
   shows "continuous_on s f \<longleftrightarrow>
     (\<forall>x. \<forall>a \<in> s. (\<forall>n. x(n) \<in> s) \<and> (x ---> a) sequentially
                     --> ((f o x) ---> f(a)) sequentially)" (is "?lhs = ?rhs")