--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Sep 24 23:51:32 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Sep 24 15:03:49 2013 -0700
@@ -1485,9 +1485,6 @@
text{* The expected monotonicity property. *}
-lemma Lim_within_empty: "(f ---> l) (at x within {})"
- unfolding tendsto_def eventually_at_filter by simp
-
lemma Lim_Un:
assumes "(f ---> l) (at x within S)" "(f ---> l) (at x within T)"
shows "(f ---> l) (at x within (S \<union> T))"
@@ -1551,7 +1548,7 @@
shows "(f ---> Inf (f ` ({x<..} \<inter> I))) (at x within ({x<..} \<inter> I))"
proof (cases "{x<..} \<inter> I = {}")
case True
- then show ?thesis by (simp add: Lim_within_empty)
+ then show ?thesis by simp
next
case False
show ?thesis