factor out new lemma
authorhuffman
Tue Sep 24 15:03:49 2013 -0700 (2013-09-24)
changeset 53860f2d683432580
parent 53859 e6cb01686f7b
child 53861 5ba90fca32bc
factor out new lemma
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Topological_Spaces.thy
     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)