src/HOL/Complex.thy
 changeset 36825 d9320cdcde73 parent 36777 be5461582d0f child 37767 a2b7a20d6ea3
```     1.1 --- a/src/HOL/Complex.thy	Tue May 11 06:30:48 2010 -0700
1.2 +++ b/src/HOL/Complex.thy	Tue May 11 07:58:48 2010 -0700
1.3 @@ -353,16 +353,26 @@
1.5  done
1.6
1.7 +lemma tendsto_Complex [tendsto_intros]:
1.8 +  assumes "(f ---> a) net" and "(g ---> b) net"
1.9 +  shows "((\<lambda>x. Complex (f x) (g x)) ---> Complex a b) net"
1.10 +proof (rule tendstoI)
1.11 +  fix r :: real assume "0 < r"
1.12 +  hence "0 < r / sqrt 2" by (simp add: divide_pos_pos)
1.13 +  have "eventually (\<lambda>x. dist (f x) a < r / sqrt 2) net"
1.14 +    using `(f ---> a) net` and `0 < r / sqrt 2` by (rule tendstoD)
1.15 +  moreover
1.16 +  have "eventually (\<lambda>x. dist (g x) b < r / sqrt 2) net"
1.17 +    using `(g ---> b) net` and `0 < r / sqrt 2` by (rule tendstoD)
1.18 +  ultimately
1.19 +  show "eventually (\<lambda>x. dist (Complex (f x) (g x)) (Complex a b) < r) net"
1.20 +    by (rule eventually_elim2)
1.21 +       (simp add: dist_norm real_sqrt_sum_squares_less)
1.22 +qed
1.23 +
1.24  lemma LIMSEQ_Complex:
1.25    "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. Complex (X n) (Y n)) ----> Complex a b"
1.26 -apply (rule LIMSEQ_I)
1.27 -apply (subgoal_tac "0 < r / sqrt 2")
1.28 -apply (drule_tac r="r / sqrt 2" in LIMSEQ_D, safe)
1.29 -apply (drule_tac r="r / sqrt 2" in LIMSEQ_D, safe)
1.30 -apply (rename_tac M N, rule_tac x="max M N" in exI, safe)