--- 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