555 theorem LIM_NSLIM_iff: "(f -- x --> L) = (f -- x --NS> L)" |
555 theorem LIM_NSLIM_iff: "(f -- x --> L) = (f -- x --NS> L)" |
556 by (blast intro: LIM_NSLIM NSLIM_LIM) |
556 by (blast intro: LIM_NSLIM NSLIM_LIM) |
557 |
557 |
558 subsubsection {* Derived theorems about @{term LIM} *} |
558 subsubsection {* Derived theorems about @{term LIM} *} |
559 |
559 |
560 lemma LIM_mult2: |
|
561 fixes l m :: "'a::real_normed_algebra" |
|
562 shows "[| f -- x --> l; g -- x --> m |] |
|
563 ==> (%x. f(x) * g(x)) -- x --> (l * m)" |
|
564 by (simp add: LIM_NSLIM_iff NSLIM_mult) |
|
565 |
|
566 lemma LIM_scaleR: |
|
567 "[| f -- x --> l; g -- x --> m |] |
|
568 ==> (%x. f(x) *# g(x)) -- x --> (l *# m)" |
|
569 by (simp add: LIM_NSLIM_iff NSLIM_scaleR) |
|
570 |
|
571 lemma LIM_add2: |
|
572 "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + g(x)) -- x --> (l + m)" |
|
573 by (simp add: LIM_NSLIM_iff NSLIM_add) |
|
574 |
|
575 lemma LIM_const2: "(%x. k) -- x --> k" |
|
576 by (simp add: LIM_NSLIM_iff) |
|
577 |
|
578 lemma LIM_minus2: "f -- a --> L ==> (%x. -f(x)) -- a --> -L" |
|
579 by (simp add: LIM_NSLIM_iff NSLIM_minus) |
|
580 |
|
581 lemma LIM_add_minus2: "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + -g(x)) -- x --> (l + -m)" |
|
582 by (simp add: LIM_NSLIM_iff NSLIM_add_minus) |
|
583 |
|
584 lemma LIM_inverse: |
560 lemma LIM_inverse: |
585 fixes L :: "'a::real_normed_div_algebra" |
561 fixes L :: "'a::real_normed_div_algebra" |
586 shows "[| f -- a --> L; L \<noteq> 0 |] |
562 shows "[| f -- a --> L; L \<noteq> 0 |] |
587 ==> (%x. inverse(f(x))) -- a --> (inverse L)" |
563 ==> (%x. inverse(f(x))) -- a --> (inverse L)" |
588 by (simp add: LIM_NSLIM_iff NSLIM_inverse) |
564 by (simp add: LIM_NSLIM_iff NSLIM_inverse) |
589 |
|
590 lemma LIM_zero2: "f -- a --> l ==> (%x. f(x) - l) -- a --> 0" |
|
591 by (simp add: LIM_NSLIM_iff NSLIM_zero) |
|
592 |
|
593 lemma LIM_unique2: |
|
594 fixes a :: real |
|
595 shows "[| f -- a --> L; f -- a --> M |] ==> L = M" |
|
596 by (simp add: LIM_NSLIM_iff NSLIM_unique) |
|
597 |
|
598 (* we can use the corresponding thm LIM_mult2 *) |
|
599 (* for standard definition of limit *) |
|
600 |
|
601 lemma LIM_mult_zero2: |
|
602 fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra" |
|
603 shows "[| f -- x --> 0; g -- x --> 0 |] ==> (%x. f(x)*g(x)) -- x --> 0" |
|
604 by (drule LIM_mult2, auto) |
|
605 |
565 |
606 |
566 |
607 subsection {* Continuity *} |
567 subsection {* Continuity *} |
608 |
568 |
609 subsubsection {* Purely standard proofs *} |
569 subsubsection {* Purely standard proofs *} |