src/HOL/Library/Euclidean_Space.thy
 changeset 31416 f4c079225845 parent 31406 e23dd3aac0fb child 31417 c12b25b7f015
```     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Wed Jun 03 08:43:29 2009 -0700
1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Wed Jun 03 08:46:13 2009 -0700
1.3 @@ -506,6 +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 open_vector_def:
1.8 +  "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y::'a ^ 'b. dist y x < e \<longrightarrow> y \<in> S)"
1.9 +
1.10  instance proof
1.11    fix x y :: "'a ^ 'b"
1.12    show "dist x y = 0 \<longleftrightarrow> x = y"
1.13 @@ -518,6 +521,10 @@
1.14      apply (rule order_trans [OF _ setL2_triangle_ineq])
1.15      apply (simp add: setL2_mono dist_triangle2)
1.16      done
1.17 +next
1.18 +  fix S :: "('a ^ 'b) set"
1.19 +  show "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
1.20 +    by (rule open_vector_def)
1.21  qed
1.22
1.23  end
```