src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 53860 f2d683432580
parent 53859 e6cb01686f7b
child 53861 5ba90fca32bc
     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>