equal
deleted
inserted
replaced
338 by (cases x) simp |
338 by (cases x) simp |
339 |
339 |
340 subsection {* Completeness of the Complexes *} |
340 subsection {* Completeness of the Complexes *} |
341 |
341 |
342 interpretation Re: bounded_linear "Re" |
342 interpretation Re: bounded_linear "Re" |
343 apply (unfold_locales, simp, simp) |
343 by (rule bounded_linear_intro [where K=1], simp_all add: complex_norm_def) |
344 apply (rule_tac x=1 in exI) |
|
345 apply (simp add: complex_norm_def) |
|
346 done |
|
347 |
344 |
348 interpretation Im: bounded_linear "Im" |
345 interpretation Im: bounded_linear "Im" |
349 apply (unfold_locales, simp, simp) |
346 by (rule bounded_linear_intro [where K=1], simp_all add: complex_norm_def) |
350 apply (rule_tac x=1 in exI) |
|
351 apply (simp add: complex_norm_def) |
|
352 done |
|
353 |
347 |
354 lemma tendsto_Complex [tendsto_intros]: |
348 lemma tendsto_Complex [tendsto_intros]: |
355 assumes "(f ---> a) net" and "(g ---> b) net" |
349 assumes "(f ---> a) net" and "(g ---> b) net" |
356 shows "((\<lambda>x. Complex (f x) (g x)) ---> Complex a b) net" |
350 shows "((\<lambda>x. Complex (f x) (g x)) ---> Complex a b) net" |
357 proof (rule tendstoI) |
351 proof (rule tendstoI) |
516 |
510 |
517 lemma complex_mod_mult_cnj: "cmod (z * cnj z) = (cmod z)\<twosuperior>" |
511 lemma complex_mod_mult_cnj: "cmod (z * cnj z) = (cmod z)\<twosuperior>" |
518 by (simp add: norm_mult power2_eq_square) |
512 by (simp add: norm_mult power2_eq_square) |
519 |
513 |
520 interpretation cnj: bounded_linear "cnj" |
514 interpretation cnj: bounded_linear "cnj" |
521 apply (unfold_locales) |
515 using complex_cnj_add complex_cnj_scaleR |
522 apply (rule complex_cnj_add) |
516 by (rule bounded_linear_intro [where K=1], simp) |
523 apply (rule complex_cnj_scaleR) |
|
524 apply (rule_tac x=1 in exI, simp) |
|
525 done |
|
526 |
517 |
527 |
518 |
528 subsection{*The Functions @{term sgn} and @{term arg}*} |
519 subsection{*The Functions @{term sgn} and @{term arg}*} |
529 |
520 |
530 text {*------------ Argand -------------*} |
521 text {*------------ Argand -------------*} |