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"
```