src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 53859 e6cb01686f7b
parent 53813 0a62ad289c4d
child 53860 f2d683432580
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Sep 24 23:51:32 2013 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Sep 24 15:03:49 2013 -0700
     1.3 @@ -1485,9 +1485,6 @@
     1.4  
     1.5  text{* The expected monotonicity property. *}
     1.6  
     1.7 -lemma Lim_within_empty: "(f ---> l) (at x within {})"
     1.8 -  unfolding tendsto_def eventually_at_filter by simp
     1.9 -
    1.10  lemma Lim_Un:
    1.11    assumes "(f ---> l) (at x within S)" "(f ---> l) (at x within T)"
    1.12    shows "(f ---> l) (at x within (S \<union> T))"
    1.13 @@ -1551,7 +1548,7 @@
    1.14    shows "(f ---> Inf (f ` ({x<..} \<inter> I))) (at x within ({x<..} \<inter> I))"
    1.15  proof (cases "{x<..} \<inter> I = {}")
    1.16    case True
    1.17 -  then show ?thesis by (simp add: Lim_within_empty)
    1.18 +  then show ?thesis by simp
    1.19  next
    1.20    case False
    1.21    show ?thesis