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.22  
    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.42  
    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.64  
    1.65  text{* Limit under bilinear function *}
    1.66