# HG changeset patch
# User huffman
# Date 1380060229 25200
# Node ID f2d6834325806391cfbc1bd34980115dc0405cb6
# Parent  e6cb01686f7bc1b594dd9951fb1a6dc6adcdbc68
factor out new lemma

diff -r e6cb01686f7b -r f2d683432580 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Sep 24 15:03:49 2013 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Sep 24 15:03:49 2013 -0700
@@ -1488,13 +1488,7 @@
 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))"
-  using assms
-  unfolding tendsto_def eventually_at_filter
-  apply clarify
-  apply (drule spec, drule (1) mp, drule (1) mp)
-  apply (drule spec, drule (1) mp, drule (1) mp)
-  apply (auto elim: eventually_elim2)
-  done
+  using assms unfolding at_within_union by (rule filterlim_sup)
 
 lemma Lim_Un_univ:
   "(f ---> l) (at x within S) \<Longrightarrow> (f ---> l) (at x within T) \<Longrightarrow>
diff -r e6cb01686f7b -r f2d683432580 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Tue Sep 24 15:03:49 2013 -0700
+++ b/src/HOL/Topological_Spaces.thy	Tue Sep 24 15:03:49 2013 -0700
@@ -757,6 +757,10 @@
 lemma at_within_empty [simp]: "at a within {} = bot"
   unfolding at_within_def by simp
 
+lemma at_within_union: "at x within (S \<union> T) = sup (at x within S) (at x within T)"
+  unfolding filter_eq_iff eventually_sup eventually_at_filter
+  by (auto elim!: eventually_rev_mp)
+
 lemma at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}"
   unfolding trivial_limit_def eventually_at_topological
   by (safe, case_tac "S = {a}", simp, fast, fast)