src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 53862 cb1094587ee4
parent 53861 5ba90fca32bc
child 54070 1a13325269c2
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Sep 24 15:03:50 2013 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Sep 24 15:03:51 2013 -0700
     1.3 @@ -1528,7 +1528,7 @@
     1.4    unfolding filter_eq_iff by (intro allI eventually_within_interior)
     1.5  
     1.6  lemma Lim_within_LIMSEQ:
     1.7 -  fixes a :: "'a::metric_space"
     1.8 +  fixes a :: "'a::first_countable_topology"
     1.9    assumes "\<forall>S. (\<forall>n. S n \<noteq> a \<and> S n \<in> T) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
    1.10    shows "(X ---> L) (at a within T)"
    1.11    using assms unfolding tendsto_def [where l=L]