# HG changeset patch
# User huffman
# Date 1244043973 25200
# Node ID f4c079225845a8956af902926521b94ebde48a27
# Parent  80686a815b59667b16f85e52c727214582cbff22
open_dist instance for vectors

diff -r 80686a815b59 -r f4c079225845 src/HOL/Library/Euclidean_Space.thy
--- a/src/HOL/Library/Euclidean_Space.thy	Wed Jun 03 08:43:29 2009 -0700
+++ b/src/HOL/Library/Euclidean_Space.thy	Wed Jun 03 08:46:13 2009 -0700
@@ -506,6 +506,9 @@
 definition dist_vector_def:
   "dist (x::'a^'b) (y::'a^'b) = setL2 (\<lambda>i. dist (x$i) (y$i)) UNIV"
 
+definition open_vector_def:
+  "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y::'a ^ 'b. dist y x < e \<longrightarrow> y \<in> S)"
+
 instance proof
   fix x y :: "'a ^ 'b"
   show "dist x y = 0 \<longleftrightarrow> x = y"
@@ -518,6 +521,10 @@
     apply (rule order_trans [OF _ setL2_triangle_ineq])
     apply (simp add: setL2_mono dist_triangle2)
     done
+next
+  fix S :: "('a ^ 'b) set"
+  show "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
+    by (rule open_vector_def)
 qed
 
 end