src/HOL/Analysis/Ordered_Euclidean_Space.thy
changeset 69632 7d02b7bee660
parent 69631 6c3e6038e74c
child 69683 8b3458ca0762
equal deleted inserted replaced
69631:6c3e6038e74c 69632:7d02b7bee660
     4 imports
     4 imports
     5   Cartesian_Euclidean_Space
     5   Cartesian_Euclidean_Space
     6   "HOL-Library.Product_Order"
     6   "HOL-Library.Product_Order"
     7 begin
     7 begin
     8 
     8 
     9 subsection%important \<open>An ordering on euclidean spaces that will allow us to talk about intervals\<close>
     9 text%important \<open>An ordering on euclidean spaces that will allow us to talk about intervals\<close>
    10 
    10 
    11 class ordered_euclidean_space = ord + inf + sup + abs + Inf + Sup + euclidean_space +
    11 class ordered_euclidean_space = ord + inf + sup + abs + Inf + Sup + euclidean_space +
    12   assumes eucl_le: "x \<le> y \<longleftrightarrow> (\<forall>i\<in>Basis. x \<bullet> i \<le> y \<bullet> i)"
    12   assumes eucl_le: "x \<le> y \<longleftrightarrow> (\<forall>i\<in>Basis. x \<bullet> i \<le> y \<bullet> i)"
    13   assumes eucl_less_le_not_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
    13   assumes eucl_less_le_not_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
    14   assumes eucl_inf: "inf x y = (\<Sum>i\<in>Basis. inf (x \<bullet> i) (y \<bullet> i) *\<^sub>R i)"
    14   assumes eucl_inf: "inf x y = (\<Sum>i\<in>Basis. inf (x \<bullet> i) (y \<bullet> i) *\<^sub>R i)"