# HG changeset patch
# User huffman
# Date 1380060231 25200
# Node ID cb1094587ee4bba72f784074137cbe76122f76df
# Parent  5ba90fca32bc3217c5b710ab5d2c63753010213f
generalize lemma

diff -r 5ba90fca32bc -r cb1094587ee4 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Sep 24 15:03:50 2013 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Sep 24 15:03:51 2013 -0700
@@ -1528,7 +1528,7 @@
   unfolding filter_eq_iff by (intro allI eventually_within_interior)
 
 lemma Lim_within_LIMSEQ:
-  fixes a :: "'a::metric_space"
+  fixes a :: "'a::first_countable_topology"
   assumes "\<forall>S. (\<forall>n. S n \<noteq> a \<and> S n \<in> T) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
   shows "(X ---> L) (at a within T)"
   using assms unfolding tendsto_def [where l=L]