author huffman Wed, 26 Mar 2014 11:05:25 -0700 changeset 56290 801a72ad52d3 parent 56289 d8d2a2b97168 child 56310 4d8955cdfb97
tuned proofs
```--- 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"
-    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"
-    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"