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