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
```