1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Aug 24 15:06:13 2011 -0700
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Aug 24 15:32:40 2011 -0700
1.3 @@ -7,7 +7,7 @@
1.4 header {* Elementary topology in Euclidean space. *}
1.5
1.6 theory Topology_Euclidean_Space
1.7 -imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs" Norm_Arith
1.8 +imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs" Norm_Arith L2_Norm
1.9 begin
1.10
1.11 (* to be moved elsewhere *)
1.12 @@ -20,7 +20,7 @@
1.13 apply(subst(2) euclidean_dist_l2) apply(cases "i<DIM('a)")
1.14 apply(rule member_le_setL2) by auto
1.15
1.16 -subsection {* General notion of a topologies as values *}
1.17 +subsection {* General notion of a topology as a value *}
1.18
1.19 definition "istopology L \<longleftrightarrow> L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union> K))"
1.20 typedef (open) 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"