# HG changeset patch
# User huffman
# Date 1395857125 25200
# Node ID 801a72ad52d399a631de6fb99bbad0a44d83443a
# Parent  d8d2a2b971682cd2d9717eb51555f54e3c47c610
tuned proofs

diff -r d8d2a2b97168 -r 801a72ad52d3 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Mar 26 14:00:37 2014 +0000
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Mar 26 11:05:25 2014 -0700
@@ -1958,39 +1958,13 @@
     and "(f ---> l) net"
     and "eventually (\<lambda>x. dist a (f x) \<le> e) net"
   shows "dist a l \<le> e"
-proof -
-  have "dist a l \<in> {..e}"
-  proof (rule Lim_in_closed_set)
-    show "closed {..e}"
-      by simp
-    show "eventually (\<lambda>x. dist a (f x) \<in> {..e}) net"
-      by (simp add: assms)
-    show "\<not> trivial_limit net"
-      by fact
-    show "((\<lambda>x. dist a (f x)) ---> dist a l) net"
-      by (intro tendsto_intros assms)
-  qed
-  then show ?thesis by simp
-qed
+  using assms by (fast intro: tendsto_le tendsto_intros)
 
 lemma Lim_norm_ubound:
   fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. norm(f x) \<le> e) net"
   shows "norm(l) \<le> e"
-proof -
-  have "norm l \<in> {..e}"
-  proof (rule Lim_in_closed_set)
-    show "closed {..e}"
-      by simp
-    show "eventually (\<lambda>x. norm (f x) \<in> {..e}) net"
-      by (simp add: assms)
-    show "\<not> trivial_limit net"
-      by fact
-    show "((\<lambda>x. norm (f x)) ---> norm l) net"
-      by (intro tendsto_intros assms)
-  qed
-  then show ?thesis by simp
-qed
+  using assms by (fast intro: tendsto_le tendsto_intros)
 
 lemma Lim_norm_lbound:
   fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
@@ -1998,20 +1972,7 @@
     and "(f ---> l) net"
     and "eventually (\<lambda>x. e \<le> norm (f x)) net"
   shows "e \<le> norm l"
-proof -
-  have "norm l \<in> {e..}"
-  proof (rule Lim_in_closed_set)
-    show "closed {e..}"
-      by simp
-    show "eventually (\<lambda>x. norm (f x) \<in> {e..}) net"
-      by (simp add: assms)
-    show "\<not> trivial_limit net"
-      by fact
-    show "((\<lambda>x. norm (f x)) ---> norm l) net"
-      by (intro tendsto_intros assms)
-  qed
-  then show ?thesis by simp
-qed
+  using assms by (fast intro: tendsto_le tendsto_intros)
 
 text{* Limit under bilinear function *}