author huffman Tue Sep 24 15:03:49 2013 -0700 (2013-09-24) changeset 53860 f2d683432580 parent 53859 e6cb01686f7b child 53861 5ba90fca32bc
factor out new lemma
```     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Sep 24 15:03:49 2013 -0700
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Sep 24 15:03:49 2013 -0700
1.3 @@ -1488,13 +1488,7 @@
1.4  lemma Lim_Un:
1.5    assumes "(f ---> l) (at x within S)" "(f ---> l) (at x within T)"
1.6    shows "(f ---> l) (at x within (S \<union> T))"
1.7 -  using assms
1.8 -  unfolding tendsto_def eventually_at_filter
1.9 -  apply clarify
1.10 -  apply (drule spec, drule (1) mp, drule (1) mp)
1.11 -  apply (drule spec, drule (1) mp, drule (1) mp)
1.12 -  apply (auto elim: eventually_elim2)
1.13 -  done
1.14 +  using assms unfolding at_within_union by (rule filterlim_sup)
1.15
1.16  lemma Lim_Un_univ:
1.17    "(f ---> l) (at x within S) \<Longrightarrow> (f ---> l) (at x within T) \<Longrightarrow>
```
```     2.1 --- a/src/HOL/Topological_Spaces.thy	Tue Sep 24 15:03:49 2013 -0700
2.2 +++ b/src/HOL/Topological_Spaces.thy	Tue Sep 24 15:03:49 2013 -0700
2.3 @@ -757,6 +757,10 @@
2.4  lemma at_within_empty [simp]: "at a within {} = bot"
2.5    unfolding at_within_def by simp
2.6
2.7 +lemma at_within_union: "at x within (S \<union> T) = sup (at x within S) (at x within T)"
2.8 +  unfolding filter_eq_iff eventually_sup eventually_at_filter
2.9 +  by (auto elim!: eventually_rev_mp)
2.10 +
2.11  lemma at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}"
2.12    unfolding trivial_limit_def eventually_at_topological
2.13    by (safe, case_tac "S = {a}", simp, fast, fast)
```