changeset 36431 | 340755027840 |
parent 36365 | 18bf20d0c2df |
child 36432 | 1ad1cfeaec2d |
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Mon Apr 26 11:08:49 2010 -0700 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Mon Apr 26 12:19:57 2010 -0700 @@ -19,7 +19,7 @@ header {* Results connected with topological dimension. *} theory Brouwer_Fixpoint - imports Convex_Euclidean_Space + imports Convex_Euclidean_Space Vec1 begin lemma brouwer_compactness_lemma: