equal
deleted
inserted
replaced
625 from this topological_tendstoD [OF f A] |
625 from this topological_tendstoD [OF f A] |
626 show "eventually (\<lambda>x. g (f x) \<in> B) F" |
626 show "eventually (\<lambda>x. g (f x) \<in> B) F" |
627 by (rule eventually_mono) |
627 by (rule eventually_mono) |
628 qed |
628 qed |
629 |
629 |
|
630 lemma metric_tendsto_imp_tendsto: |
|
631 assumes f: "(f ---> a) F" |
|
632 assumes le: "eventually (\<lambda>x. dist (g x) b \<le> dist (f x) a) F" |
|
633 shows "(g ---> b) F" |
|
634 proof (rule tendstoI) |
|
635 fix e :: real assume "0 < e" |
|
636 with f have "eventually (\<lambda>x. dist (f x) a < e) F" by (rule tendstoD) |
|
637 with le show "eventually (\<lambda>x. dist (g x) b < e) F" |
|
638 using le_less_trans by (rule eventually_elim2) |
|
639 qed |
|
640 |
630 subsubsection {* Distance and norms *} |
641 subsubsection {* Distance and norms *} |
631 |
642 |
632 lemma tendsto_dist [tendsto_intros]: |
643 lemma tendsto_dist [tendsto_intros]: |
633 assumes f: "(f ---> l) F" and g: "(g ---> m) F" |
644 assumes f: "(f ---> l) F" and g: "(g ---> m) F" |
634 shows "((\<lambda>x. dist (f x) (g x)) ---> dist l m) F" |
645 shows "((\<lambda>x. dist (f x) (g x)) ---> dist l m) F" |