src/HOL/Library/Euclidean_Space.thy
changeset 31492 5400beeddb55
parent 31445 c8a474a919a7
child 31493 d92cfed6c6b2
     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Sun Jun 07 15:18:52 2009 -0700
     1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Sun Jun 07 17:59:54 2009 -0700
     1.3 @@ -506,8 +506,9 @@
     1.4  definition dist_vector_def:
     1.5    "dist (x::'a^'b) (y::'a^'b) = setL2 (\<lambda>i. dist (x$i) (y$i)) UNIV"
     1.6  
     1.7 -definition topo_vector_def:
     1.8 -  "topo = {S::('a ^ 'b) set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
     1.9 +definition open_vector_def:
    1.10 +  "open (S :: ('a ^ 'b) set) \<longleftrightarrow>
    1.11 +    (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
    1.12  
    1.13  instance proof
    1.14    fix x y :: "'a ^ 'b"
    1.15 @@ -522,8 +523,9 @@
    1.16      apply (simp add: setL2_mono dist_triangle2)
    1.17      done
    1.18  next
    1.19 -  show "topo = {S::('a ^ 'b) set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
    1.20 -    by (rule topo_vector_def)
    1.21 +  fix S :: "('a ^ 'b) set"
    1.22 +  show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
    1.23 +    by (rule open_vector_def)
    1.24  qed
    1.25  
    1.26  end