579 unfolding tendsto_def eventually_within eventually_at_topological by auto |
579 unfolding tendsto_def eventually_within eventually_at_topological by auto |
580 |
580 |
581 lemma tendsto_const [tendsto_intros]: "((\<lambda>x. k) ---> k) F" |
581 lemma tendsto_const [tendsto_intros]: "((\<lambda>x. k) ---> k) F" |
582 by (simp add: tendsto_def) |
582 by (simp add: tendsto_def) |
583 |
583 |
|
584 lemma tendsto_unique: |
|
585 fixes f :: "'a \<Rightarrow> 'b::t2_space" |
|
586 assumes "\<not> trivial_limit F" and "(f ---> a) F" and "(f ---> b) F" |
|
587 shows "a = b" |
|
588 proof (rule ccontr) |
|
589 assume "a \<noteq> b" |
|
590 obtain U V where "open U" "open V" "a \<in> U" "b \<in> V" "U \<inter> V = {}" |
|
591 using hausdorff [OF `a \<noteq> b`] by fast |
|
592 have "eventually (\<lambda>x. f x \<in> U) F" |
|
593 using `(f ---> a) F` `open U` `a \<in> U` by (rule topological_tendstoD) |
|
594 moreover |
|
595 have "eventually (\<lambda>x. f x \<in> V) F" |
|
596 using `(f ---> b) F` `open V` `b \<in> V` by (rule topological_tendstoD) |
|
597 ultimately |
|
598 have "eventually (\<lambda>x. False) F" |
|
599 proof (rule eventually_elim2) |
|
600 fix x |
|
601 assume "f x \<in> U" "f x \<in> V" |
|
602 hence "f x \<in> U \<inter> V" by simp |
|
603 with `U \<inter> V = {}` show "False" by simp |
|
604 qed |
|
605 with `\<not> trivial_limit F` show "False" |
|
606 by (simp add: trivial_limit_def) |
|
607 qed |
|
608 |
584 lemma tendsto_const_iff: |
609 lemma tendsto_const_iff: |
585 fixes k l :: "'a::metric_space" |
610 fixes a b :: "'a::t2_space" |
586 assumes "F \<noteq> bot" shows "((\<lambda>n. k) ---> l) F \<longleftrightarrow> k = l" |
611 assumes "\<not> trivial_limit F" shows "((\<lambda>x. a) ---> b) F \<longleftrightarrow> a = b" |
587 apply (safe intro!: tendsto_const) |
612 by (safe intro!: tendsto_const tendsto_unique [OF assms tendsto_const]) |
588 apply (rule ccontr) |
613 |
589 apply (drule_tac e="dist k l" in tendstoD) |
614 subsubsection {* Distance and norms *} |
590 apply (simp add: zero_less_dist_iff) |
|
591 apply (simp add: eventually_False assms) |
|
592 done |
|
593 |
615 |
594 lemma tendsto_dist [tendsto_intros]: |
616 lemma tendsto_dist [tendsto_intros]: |
595 assumes f: "(f ---> l) F" and g: "(g ---> m) F" |
617 assumes f: "(f ---> l) F" and g: "(g ---> m) F" |
596 shows "((\<lambda>x. dist (f x) (g x)) ---> dist l m) F" |
618 shows "((\<lambda>x. dist (f x) (g x)) ---> dist l m) F" |
597 proof (rule tendstoI) |
619 proof (rule tendstoI) |
608 using dist_triangle3 [of "l" "m" "f x"] |
630 using dist_triangle3 [of "l" "m" "f x"] |
609 using dist_triangle [of "f x" "m" "g x"] |
631 using dist_triangle [of "f x" "m" "g x"] |
610 by arith |
632 by arith |
611 qed |
633 qed |
612 qed |
634 qed |
613 |
|
614 subsubsection {* Norms *} |
|
615 |
635 |
616 lemma norm_conv_dist: "norm x = dist x 0" |
636 lemma norm_conv_dist: "norm x = dist x 0" |
617 unfolding dist_norm by simp |
637 unfolding dist_norm by simp |
618 |
638 |
619 lemma tendsto_norm [tendsto_intros]: |
639 lemma tendsto_norm [tendsto_intros]: |
863 lemma tendsto_sgn [tendsto_intros]: |
883 lemma tendsto_sgn [tendsto_intros]: |
864 fixes l :: "'a::real_normed_vector" |
884 fixes l :: "'a::real_normed_vector" |
865 shows "\<lbrakk>(f ---> l) F; l \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. sgn (f x)) ---> sgn l) F" |
885 shows "\<lbrakk>(f ---> l) F; l \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. sgn (f x)) ---> sgn l) F" |
866 unfolding sgn_div_norm by (simp add: tendsto_intros) |
886 unfolding sgn_div_norm by (simp add: tendsto_intros) |
867 |
887 |
868 subsubsection {* Uniqueness *} |
|
869 |
|
870 lemma tendsto_unique: |
|
871 fixes f :: "'a \<Rightarrow> 'b::t2_space" |
|
872 assumes "\<not> trivial_limit F" "(f ---> l) F" "(f ---> l') F" |
|
873 shows "l = l'" |
|
874 proof (rule ccontr) |
|
875 assume "l \<noteq> l'" |
|
876 obtain U V where "open U" "open V" "l \<in> U" "l' \<in> V" "U \<inter> V = {}" |
|
877 using hausdorff [OF `l \<noteq> l'`] by fast |
|
878 have "eventually (\<lambda>x. f x \<in> U) F" |
|
879 using `(f ---> l) F` `open U` `l \<in> U` by (rule topological_tendstoD) |
|
880 moreover |
|
881 have "eventually (\<lambda>x. f x \<in> V) F" |
|
882 using `(f ---> l') F` `open V` `l' \<in> V` by (rule topological_tendstoD) |
|
883 ultimately |
|
884 have "eventually (\<lambda>x. False) F" |
|
885 proof (rule eventually_elim2) |
|
886 fix x |
|
887 assume "f x \<in> U" "f x \<in> V" |
|
888 hence "f x \<in> U \<inter> V" by simp |
|
889 with `U \<inter> V = {}` show "False" by simp |
|
890 qed |
|
891 with `\<not> trivial_limit F` show "False" |
|
892 by (simp add: trivial_limit_def) |
|
893 qed |
|
894 |
|
895 end |
888 end |