--- 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>
--- 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)