src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 51472 adb441e4b9e9
parent 51471 cad22a3cc09c
child 51473 1210309fddab
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Mar 22 10:41:42 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Mar 22 10:41:43 2013 +0100
     1.3 @@ -1416,7 +1416,7 @@
     1.4    unfolding tendsto_def Limits.eventually_within by simp
     1.5  
     1.6  lemma Lim_within_subset: "(f ---> l) (net within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f ---> l) (net within T)"
     1.7 -  unfolding tendsto_def Limits.eventually_within
     1.8 +  unfolding tendsto_def Topological_Spaces.eventually_within
     1.9    by (auto elim!: eventually_elim1)
    1.10  
    1.11  lemma Lim_Un: assumes "(f ---> l) (net within S)" "(f ---> l) (net within T)"
    1.12 @@ -4667,7 +4667,7 @@
    1.13    hence "eventually (\<lambda>y. f y \<noteq> a) (at x within s)"
    1.14      using `a \<notin> U` by (fast elim: eventually_mono [rotated])
    1.15    thus ?thesis
    1.16 -    unfolding Limits.eventually_within Limits.eventually_at
    1.17 +    unfolding Limits.eventually_within Metric_Spaces.eventually_at
    1.18      by (rule ex_forward, cut_tac `f x \<noteq> a`, auto simp: dist_commute)
    1.19  qed
    1.20