src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 44628 bd17b7543af1
parent 44584 08ad27488983
child 44632 076a45f65e12
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 31 07:51:55 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 31 08:11:47 2011 -0700
     1.3 @@ -7,19 +7,9 @@
     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 L2_Norm
     1.8 +imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs" Norm_Arith
     1.9  begin
    1.10  
    1.11 -(* to be moved elsewhere *)
    1.12 -
    1.13 -lemma euclidean_dist_l2:"dist x (y::'a::euclidean_space) = setL2 (\<lambda>i. dist(x$$i) (y$$i)) {..<DIM('a)}"
    1.14 -  unfolding dist_norm norm_eq_sqrt_inner setL2_def apply(subst euclidean_inner)
    1.15 -  by(auto simp add:power2_eq_square)
    1.16 -
    1.17 -lemma dist_nth_le: "dist (x $$ i) (y $$ i) \<le> dist x (y::'a::euclidean_space)"
    1.18 -  apply(subst(2) euclidean_dist_l2) apply(cases "i<DIM('a)")
    1.19 -  apply(rule member_le_setL2) by auto
    1.20 -
    1.21  subsection {* General notion of a topology as a value *}
    1.22  
    1.23  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))"