# HG changeset patch
# User huffman
# Date 1273589928 25200
# Node ID d9320cdcde73a607a84bacb208a729bf93f1c5cd
# Parent  2e9a866141b8f0f4f298948a06e54bd689770f3e
add lemma tendsto_Complex

diff -r 2e9a866141b8 -r d9320cdcde73 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Tue May 11 06:30:48 2010 -0700
+++ b/src/HOL/Complex.thy	Tue May 11 07:58:48 2010 -0700
@@ -353,16 +353,26 @@
 apply (simp add: complex_norm_def)
 done
 
+lemma tendsto_Complex [tendsto_intros]:
+  assumes "(f ---> a) net" and "(g ---> b) net"
+  shows "((\<lambda>x. Complex (f x) (g x)) ---> Complex a b) net"
+proof (rule tendstoI)
+  fix r :: real assume "0 < r"
+  hence "0 < r / sqrt 2" by (simp add: divide_pos_pos)
+  have "eventually (\<lambda>x. dist (f x) a < r / sqrt 2) net"
+    using `(f ---> a) net` and `0 < r / sqrt 2` by (rule tendstoD)
+  moreover
+  have "eventually (\<lambda>x. dist (g x) b < r / sqrt 2) net"
+    using `(g ---> b) net` and `0 < r / sqrt 2` by (rule tendstoD)
+  ultimately
+  show "eventually (\<lambda>x. dist (Complex (f x) (g x)) (Complex a b) < r) net"
+    by (rule eventually_elim2)
+       (simp add: dist_norm real_sqrt_sum_squares_less)
+qed
+
 lemma LIMSEQ_Complex:
   "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. Complex (X n) (Y n)) ----> Complex a b"
-apply (rule LIMSEQ_I)
-apply (subgoal_tac "0 < r / sqrt 2")
-apply (drule_tac r="r / sqrt 2" in LIMSEQ_D, safe)
-apply (drule_tac r="r / sqrt 2" in LIMSEQ_D, safe)
-apply (rename_tac M N, rule_tac x="max M N" in exI, safe)
-apply (simp add: real_sqrt_sum_squares_less)
-apply (simp add: divide_pos_pos)
-done
+by (rule tendsto_Complex)
 
 instance complex :: banach
 proof