# HG changeset patch
# User hoelzl
# Date 1362585381 -3600
# Node ID 6b5250100db8243adc371e4e9a9282ead1515585
# Parent  8ee3778235185e401708b3ba17f80e4f2837f3b5
netlimit is abbreviation for Lim

diff -r 8ee377823518 -r 6b5250100db8 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Mar 06 16:56:21 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Mar 06 16:56:21 2013 +0100
@@ -1376,6 +1376,13 @@
 definition Lim :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b::t2_space) \<Rightarrow> 'b"
   where "Lim A f = (THE l. (f ---> l) A)"
 
+text{* Uniqueness of the limit, when nontrivial. *}
+
+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 tendsto_unique[of net f] by auto
+
 lemma Lim:
  "(f ---> l) net \<longleftrightarrow>
         trivial_limit net \<or>
@@ -1638,13 +1645,6 @@
   thus ?thesis by simp
 qed
 
-text{* Uniqueness of the limit, when nontrivial. *}
-
-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 tendsto_unique[of net f] by auto
-
 text{* Limit under bilinear function *}
 
 lemma Lim_bilinear:
@@ -1669,21 +1669,12 @@
 
 text{* It's also sometimes useful to extract the limit point from the filter. *}
 
-definition
-  netlimit :: "'a::t2_space filter \<Rightarrow> 'a" where
-  "netlimit net = (SOME a. ((\<lambda>x. x) ---> a) net)"
+abbreviation netlimit :: "'a::t2_space filter \<Rightarrow> 'a" where
+  "netlimit F \<equiv> Lim F (\<lambda>x. x)"
 
 lemma netlimit_within:
-  assumes "\<not> trivial_limit (at a within S)"
-  shows "netlimit (at a within S) = a"
-unfolding netlimit_def
-apply (rule some_equality)
-apply (rule Lim_at_within)
-apply (rule tendsto_ident_at)
-apply (erule tendsto_unique [OF assms])
-apply (rule Lim_at_within)
-apply (rule tendsto_ident_at)
-done
+  "\<not> trivial_limit (at a within S) \<Longrightarrow> netlimit (at a within S) = a"
+  by (rule tendsto_Lim) (auto intro: tendsto_intros)
 
 lemma netlimit_at:
   fixes a :: "'a::{perfect_space,t2_space}"
@@ -6782,4 +6773,5 @@
 
 declare tendsto_const [intro] (* FIXME: move *)
 
+
 end