src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 56188 0268784f60da
parent 56166 9a241bc276cd
child 56189 c4daa97ac57a
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Mar 17 21:56:32 2014 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 18 10:12:57 2014 +0100
     1.3 @@ -826,10 +826,23 @@
     1.4    where "eucl_less a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i)"
     1.5  
     1.6  definition box_eucl_less: "box a b = {x. a <e x \<and> x <e b}"
     1.7 +definition "cbox a b = {x. \<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i}"
     1.8  
     1.9  lemma box_def: "box a b = {x. \<forall>i\<in>Basis. a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i}"
    1.10    and in_box_eucl_less: "x \<in> box a b \<longleftrightarrow> a <e x \<and> x <e b"
    1.11 -  by (auto simp: box_eucl_less eucl_less_def)
    1.12 +  and mem_box: "x \<in> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i)"
    1.13 +    "x \<in> cbox a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i)"
    1.14 +  by (auto simp: box_eucl_less eucl_less_def cbox_def)
    1.15 +
    1.16 +lemma mem_box_real[simp]:
    1.17 +  "(x::real) \<in> box a b \<longleftrightarrow> a < x \<and> x < b"
    1.18 +  "(x::real) \<in> cbox a b \<longleftrightarrow> a \<le> x \<and> x \<le> b"
    1.19 +  by (auto simp: mem_box)
    1.20 +
    1.21 +lemma box_real[simp]:
    1.22 +  fixes a b:: real
    1.23 +  shows "box a b = {a <..< b}" "cbox a b = {a .. b}"
    1.24 +  by auto
    1.25  
    1.26  lemma rational_boxes:
    1.27    fixes x :: "'a\<Colon>euclidean_space"