src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
 changeset 56290 801a72ad52d3 parent 56189 c4daa97ac57a child 56371 fb9ae0727548
1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Mar 26 14:00:37 2014 +0000
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Mar 26 11:05:25 2014 -0700
1.3 @@ -1958,39 +1958,13 @@
1.4      and "(f ---> l) net"
1.5      and "eventually (\<lambda>x. dist a (f x) \<le> e) net"
1.6    shows "dist a l \<le> e"
1.7 -proof -
1.8 -  have "dist a l \<in> {..e}"
1.9 -  proof (rule Lim_in_closed_set)
1.10 -    show "closed {..e}"
1.11 -      by simp
1.12 -    show "eventually (\<lambda>x. dist a (f x) \<in> {..e}) net"
1.13 -      by (simp add: assms)
1.14 -    show "\<not> trivial_limit net"
1.15 -      by fact
1.16 -    show "((\<lambda>x. dist a (f x)) ---> dist a l) net"
1.17 -      by (intro tendsto_intros assms)
1.18 -  qed
1.19 -  then show ?thesis by simp
1.20 -qed
1.21 +  using assms by (fast intro: tendsto_le tendsto_intros)
1.23  lemma Lim_norm_ubound:
1.24    fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
1.25    assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. norm(f x) \<le> e) net"
1.26    shows "norm(l) \<le> e"
1.27 -proof -
1.28 -  have "norm l \<in> {..e}"
1.29 -  proof (rule Lim_in_closed_set)
1.30 -    show "closed {..e}"
1.31 -      by simp
1.32 -    show "eventually (\<lambda>x. norm (f x) \<in> {..e}) net"
1.33 -      by (simp add: assms)
1.34 -    show "\<not> trivial_limit net"
1.35 -      by fact
1.36 -    show "((\<lambda>x. norm (f x)) ---> norm l) net"
1.37 -      by (intro tendsto_intros assms)
1.38 -  qed
1.39 -  then show ?thesis by simp
1.40 -qed
1.41 +  using assms by (fast intro: tendsto_le tendsto_intros)
1.43  lemma Lim_norm_lbound:
1.44    fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
1.45 @@ -1998,20 +1972,7 @@
1.46      and "(f ---> l) net"
1.47      and "eventually (\<lambda>x. e \<le> norm (f x)) net"
1.48    shows "e \<le> norm l"
1.49 -proof -
1.50 -  have "norm l \<in> {e..}"
1.51 -  proof (rule Lim_in_closed_set)
1.52 -    show "closed {e..}"
1.53 -      by simp
1.54 -    show "eventually (\<lambda>x. norm (f x) \<in> {e..}) net"
1.55 -      by (simp add: assms)
1.56 -    show "\<not> trivial_limit net"
1.57 -      by fact
1.58 -    show "((\<lambda>x. norm (f x)) ---> norm l) net"
1.59 -      by (intro tendsto_intros assms)
1.60 -  qed
1.61 -  then show ?thesis by simp
1.62 -qed
1.63 +  using assms by (fast intro: tendsto_le tendsto_intros)
1.65  text{* Limit under bilinear function *}