src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy

   then show "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x \<and> Q x" ..
 qed auto
 
 text {* Identify Trivial limits, where we can't approach arbitrarily closely. *}
 
-definition
-  trivial_limit :: "'a net \<Rightarrow> bool" where
-  "trivial_limit net \<longleftrightarrow> eventually (\<lambda>x. False) net"
-
 lemma trivial_limit_within:
   shows "trivial_limit (at a within S) \<longleftrightarrow> \<not> a islimpt S"
 proof
   assume "trivial_limit (at a within S)"
   thus "\<not> a islimpt S"

   apply clarsimp
   apply (rule_tac x="scaleR b (sgn 1)" in exI)
   apply (simp add: norm_sgn)
   done
 
-lemma trivial_limit_sequentially[intro]: "\<not> trivial_limit sequentially"
-  by (auto simp add: trivial_limit_def eventually_sequentially)
-
 text {* Some property holds "sufficiently close" to the limit point. *}
 
 lemma eventually_at: (* FIXME: this replaces Limits.eventually_at *)
   "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
 unfolding eventually_at dist_nz by auto

 lemma trivial_limit_eventually: "trivial_limit net \<Longrightarrow> eventually P net"
   unfolding trivial_limit_def by (auto elim: eventually_rev_mp)
 
 lemma eventually_False: "eventually (\<lambda>x. False) net \<longleftrightarrow> trivial_limit net"
   unfolding trivial_limit_def ..
+
 
 lemma trivial_limit_eq: "trivial_limit net \<longleftrightarrow> (\<forall>P. eventually P net)"
   apply (safe elim!: trivial_limit_eventually)
   apply (simp add: eventually_False [symmetric])
   done

   thus False by simp
 qed
 
 text{* Uniqueness of the limit, when nontrivial. *}
 
-lemma Lim_unique:
-  fixes f :: "'a \<Rightarrow> 'b::t2_space"
-  assumes "\<not> trivial_limit net"  "(f ---> l) net"  "(f ---> l') net"
-  shows "l = l'"
-proof (rule ccontr)
-  assume "l \<noteq> l'"
-  obtain U V where "open U" "open V" "l \<in> U" "l' \<in> V" "U \<inter> V = {}"
-    using hausdorff [OF `l \<noteq> l'`] by fast
-  have "eventually (\<lambda>x. f x \<in> U) net"
-    using `(f ---> l) net` `open U` `l \<in> U` by (rule topological_tendstoD)
-  moreover
-  have "eventually (\<lambda>x. f x \<in> V) net"
-    using `(f ---> l') net` `open V` `l' \<in> V` by (rule topological_tendstoD)
-  ultimately
-  have "eventually (\<lambda>x. False) net"
-  proof (rule eventually_elim2)
-    fix x
-    assume "f x \<in> U" "f x \<in> V"
-    hence "f x \<in> U \<inter> V" by simp
-    with `U \<inter> V = {}` show "False" by simp
-  qed
-  with `\<not> trivial_limit net` show "False"
-    by (simp add: eventually_False)
-qed
-
 lemma tendsto_Lim:
   fixes f :: "'a \<Rightarrow> 'b::t2_space"
   shows "~(trivial_limit net) \<Longrightarrow> (f ---> l) net ==> Lim net f = l"
-  unfolding Lim_def using Lim_unique[of net f] by auto
+  unfolding Lim_def using tendsto_unique[of net f] by auto
 
 text{* Limit under bilinear function *}
 
 lemma Lim_bilinear:
   assumes "(f ---> l) net" and "(g ---> m) net" and "bounded_bilinear h"

   shows "netlimit (at a within S) = a"
 unfolding netlimit_def
 apply (rule some_equality)
 apply (rule Lim_at_within)
 apply (rule Lim_ident_at)
-apply (erule Lim_unique [OF assms])
+apply (erule tendsto_unique [OF assms])
 apply (rule Lim_at_within)
 apply (rule Lim_ident_at)
 done
 
 lemma netlimit_at:

   { fix x assume "x islimpt s"
     then obtain f where f: "\<forall>n. f n \<in> s - {x}" "(f ---> x) sequentially"
       unfolding islimpt_sequential by auto
     then obtain l where l: "l\<in>s" "(f ---> l) sequentially"
       using `complete s`[unfolded complete_def] using convergent_imp_cauchy[of f x] by auto
-    hence "x \<in> s"  using Lim_unique[of sequentially f l x] trivial_limit_sequentially f(2) by auto
+    hence "x \<in> s"  using tendsto_unique[of sequentially f l x] trivial_limit_sequentially f(2) by auto
   }
   thus "closed s" unfolding closed_limpt by auto
 qed
 
 lemma complete_eq_closed:

 proof-
   obtain l' where l:"\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist (s n x) (l' x) < e"
     using assms(1) unfolding uniformly_convergent_eq_cauchy[THEN sym] by auto
   moreover
   { fix x assume "P x"
-    hence "l x = l' x" using Lim_unique[OF trivial_limit_sequentially, of "\<lambda>n. s n x" "l x" "l' x"]
+    hence "l x = l' x" using tendsto_unique[OF trivial_limit_sequentially, of "\<lambda>n. s n x" "l x" "l' x"]
       using l and assms(2) unfolding Lim_sequentially by blast  }
   ultimately show ?thesis by auto
 qed
 
 subsection {* Continuity *}

   hence "continuous_on s g" unfolding continuous_on_iff by auto
 
   hence "((snd \<circ> h \<circ> r) ---> g a) sequentially" unfolding continuous_on_sequentially
     apply (rule allE[where x="\<lambda>n. (fst \<circ> h \<circ> r) n"]) apply (erule ballE[where x=a])
     using lima unfolding h_def o_def using fs[OF `x\<in>s`] by (auto simp add: y_def)
-  hence "g a = a" using Lim_unique[OF trivial_limit_sequentially limb, of "g a"]
+  hence "g a = a" using tendsto_unique[OF trivial_limit_sequentially limb, of "g a"]
     unfolding `a=b` and o_assoc by auto
   moreover
   { fix x assume "x\<in>s" "g x = x" "x\<noteq>a"
     hence "False" using dist[THEN bspec[where x=a], THEN bspec[where x=x]]
       using `g a = a` and `a\<in>s` by auto  }