src/HOL/Limits.thy
changeset 44205 18da2a87421c
parent 44195 f5363511b212
child 44206 5e4a1664106e
     1.1 --- a/src/HOL/Limits.thy	Sun Aug 14 08:45:38 2011 -0700
     1.2 +++ b/src/HOL/Limits.thy	Sun Aug 14 10:25:43 2011 -0700
     1.3 @@ -581,15 +581,37 @@
     1.4  lemma tendsto_const [tendsto_intros]: "((\<lambda>x. k) ---> k) F"
     1.5    by (simp add: tendsto_def)
     1.6  
     1.7 +lemma tendsto_unique:
     1.8 +  fixes f :: "'a \<Rightarrow> 'b::t2_space"
     1.9 +  assumes "\<not> trivial_limit F" and "(f ---> a) F" and "(f ---> b) F"
    1.10 +  shows "a = b"
    1.11 +proof (rule ccontr)
    1.12 +  assume "a \<noteq> b"
    1.13 +  obtain U V where "open U" "open V" "a \<in> U" "b \<in> V" "U \<inter> V = {}"
    1.14 +    using hausdorff [OF `a \<noteq> b`] by fast
    1.15 +  have "eventually (\<lambda>x. f x \<in> U) F"
    1.16 +    using `(f ---> a) F` `open U` `a \<in> U` by (rule topological_tendstoD)
    1.17 +  moreover
    1.18 +  have "eventually (\<lambda>x. f x \<in> V) F"
    1.19 +    using `(f ---> b) F` `open V` `b \<in> V` by (rule topological_tendstoD)
    1.20 +  ultimately
    1.21 +  have "eventually (\<lambda>x. False) F"
    1.22 +  proof (rule eventually_elim2)
    1.23 +    fix x
    1.24 +    assume "f x \<in> U" "f x \<in> V"
    1.25 +    hence "f x \<in> U \<inter> V" by simp
    1.26 +    with `U \<inter> V = {}` show "False" by simp
    1.27 +  qed
    1.28 +  with `\<not> trivial_limit F` show "False"
    1.29 +    by (simp add: trivial_limit_def)
    1.30 +qed
    1.31 +
    1.32  lemma tendsto_const_iff:
    1.33 -  fixes k l :: "'a::metric_space"
    1.34 -  assumes "F \<noteq> bot" shows "((\<lambda>n. k) ---> l) F \<longleftrightarrow> k = l"
    1.35 -  apply (safe intro!: tendsto_const)
    1.36 -  apply (rule ccontr)
    1.37 -  apply (drule_tac e="dist k l" in tendstoD)
    1.38 -  apply (simp add: zero_less_dist_iff)
    1.39 -  apply (simp add: eventually_False assms)
    1.40 -  done
    1.41 +  fixes a b :: "'a::t2_space"
    1.42 +  assumes "\<not> trivial_limit F" shows "((\<lambda>x. a) ---> b) F \<longleftrightarrow> a = b"
    1.43 +  by (safe intro!: tendsto_const tendsto_unique [OF assms tendsto_const])
    1.44 +
    1.45 +subsubsection {* Distance and norms *}
    1.46  
    1.47  lemma tendsto_dist [tendsto_intros]:
    1.48    assumes f: "(f ---> l) F" and g: "(g ---> m) F"
    1.49 @@ -611,8 +633,6 @@
    1.50    qed
    1.51  qed
    1.52  
    1.53 -subsubsection {* Norms *}
    1.54 -
    1.55  lemma norm_conv_dist: "norm x = dist x 0"
    1.56    unfolding dist_norm by simp
    1.57  
    1.58 @@ -865,31 +885,4 @@
    1.59    shows "\<lbrakk>(f ---> l) F; l \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. sgn (f x)) ---> sgn l) F"
    1.60    unfolding sgn_div_norm by (simp add: tendsto_intros)
    1.61  
    1.62 -subsubsection {* Uniqueness *}
    1.63 -
    1.64 -lemma tendsto_unique:
    1.65 -  fixes f :: "'a \<Rightarrow> 'b::t2_space"
    1.66 -  assumes "\<not> trivial_limit F"  "(f ---> l) F"  "(f ---> l') F"
    1.67 -  shows "l = l'"
    1.68 -proof (rule ccontr)
    1.69 -  assume "l \<noteq> l'"
    1.70 -  obtain U V where "open U" "open V" "l \<in> U" "l' \<in> V" "U \<inter> V = {}"
    1.71 -    using hausdorff [OF `l \<noteq> l'`] by fast
    1.72 -  have "eventually (\<lambda>x. f x \<in> U) F"
    1.73 -    using `(f ---> l) F` `open U` `l \<in> U` by (rule topological_tendstoD)
    1.74 -  moreover
    1.75 -  have "eventually (\<lambda>x. f x \<in> V) F"
    1.76 -    using `(f ---> l') F` `open V` `l' \<in> V` by (rule topological_tendstoD)
    1.77 -  ultimately
    1.78 -  have "eventually (\<lambda>x. False) F"
    1.79 -  proof (rule eventually_elim2)
    1.80 -    fix x
    1.81 -    assume "f x \<in> U" "f x \<in> V"
    1.82 -    hence "f x \<in> U \<inter> V" by simp
    1.83 -    with `U \<inter> V = {}` show "False" by simp
    1.84 -  qed
    1.85 -  with `\<not> trivial_limit F` show "False"
    1.86 -    by (simp add: trivial_limit_def)
    1.87 -qed
    1.88 -
    1.89  end