# 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 "((\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 (\x. dist (f x) a < r / sqrt 2) net" + using `(f ---> a) net` and `0 < r / sqrt 2` by (rule tendstoD) + moreover + have "eventually (\x. dist (g x) b < r / sqrt 2) net" + using `(g ---> b) net` and `0 < r / sqrt 2` by (rule tendstoD) + ultimately + show "eventually (\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: "\X ----> a; Y ----> b\ \ (\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