author | haftmann |
Tue, 05 Mar 2019 07:00:21 +0000 | |
changeset 69861 | 62e47f06d22c |
parent 69730 | 0c3dcb3a17f6 |
child 69874 | 11065b70407d |
permissions | -rw-r--r-- |
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
1 |
subsection \<open>Ordered Euclidean Space\<close> (* why not Section? *) |
69631 | 2 |
|
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
3 |
theory Ordered_Euclidean_Space |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
4 |
imports |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
5 |
Cartesian_Euclidean_Space |
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
64758
diff
changeset
|
6 |
"HOL-Library.Product_Order" |
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
7 |
begin |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
8 |
|
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
9 |
text \<open>An ordering on euclidean spaces that will allow us to talk about intervals\<close> |
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
10 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
11 |
class ordered_euclidean_space = ord + inf + sup + abs + Inf + Sup + euclidean_space + |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
12 |
assumes eucl_le: "x \<le> y \<longleftrightarrow> (\<forall>i\<in>Basis. x \<bullet> i \<le> y \<bullet> i)" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
13 |
assumes eucl_less_le_not_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
14 |
assumes eucl_inf: "inf x y = (\<Sum>i\<in>Basis. inf (x \<bullet> i) (y \<bullet> i) *\<^sub>R i)" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
15 |
assumes eucl_sup: "sup x y = (\<Sum>i\<in>Basis. sup (x \<bullet> i) (y \<bullet> i) *\<^sub>R i)" |
69260
0a9688695a1b
removed relics of ASCII syntax for indexed big operators
haftmann
parents:
69000
diff
changeset
|
16 |
assumes eucl_Inf: "Inf X = (\<Sum>i\<in>Basis. (INF x\<in>X. x \<bullet> i) *\<^sub>R i)" |
0a9688695a1b
removed relics of ASCII syntax for indexed big operators
haftmann
parents:
69000
diff
changeset
|
17 |
assumes eucl_Sup: "Sup X = (\<Sum>i\<in>Basis. (SUP x\<in>X. x \<bullet> i) *\<^sub>R i)" |
61945 | 18 |
assumes eucl_abs: "\<bar>x\<bar> = (\<Sum>i\<in>Basis. \<bar>x \<bullet> i\<bar> *\<^sub>R i)" |
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
19 |
begin |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
20 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
21 |
subclass order |
61169 | 22 |
by standard |
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
23 |
(auto simp: eucl_le eucl_less_le_not_le intro!: euclidean_eqI antisym intro: order.trans) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
24 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
25 |
subclass ordered_ab_group_add_abs |
61169 | 26 |
by standard (auto simp: eucl_le inner_add_left eucl_abs abs_leI) |
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
27 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
28 |
subclass ordered_real_vector |
61169 | 29 |
by standard (auto simp: eucl_le intro!: mult_left_mono mult_right_mono) |
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
30 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
31 |
subclass lattice |
61169 | 32 |
by standard (auto simp: eucl_inf eucl_sup eucl_le) |
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
33 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
34 |
subclass distrib_lattice |
61169 | 35 |
by standard (auto simp: eucl_inf eucl_sup sup_inf_distrib1 intro!: euclidean_eqI) |
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
36 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
37 |
subclass conditionally_complete_lattice |
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
38 |
proof |
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
39 |
fix z::'a and X::"'a set" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
40 |
assume "X \<noteq> {}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
41 |
hence "\<And>i. (\<lambda>x. x \<bullet> i) ` X \<noteq> {}" by simp |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
42 |
thus "(\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> Inf X" "(\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X \<le> z" |
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
61945
diff
changeset
|
43 |
by (auto simp: eucl_Inf eucl_Sup eucl_le |
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
44 |
intro!: cInf_greatest cSup_least) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
45 |
qed (force intro!: cInf_lower cSup_upper |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
46 |
simp: bdd_below_def bdd_above_def preorder_class.bdd_below_def preorder_class.bdd_above_def |
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
61945
diff
changeset
|
47 |
eucl_Inf eucl_Sup eucl_le)+ |
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
48 |
|
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
49 |
lemma inner_Basis_inf_left: "i \<in> Basis \<Longrightarrow> inf x y \<bullet> i = inf (x \<bullet> i) (y \<bullet> i)" |
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
50 |
and inner_Basis_sup_left: "i \<in> Basis \<Longrightarrow> sup x y \<bullet> i = sup (x \<bullet> i) (y \<bullet> i)" |
64267 | 51 |
by (simp_all add: eucl_inf eucl_sup inner_sum_left inner_Basis if_distrib comm_monoid_add_class.sum.delta |
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
52 |
cong: if_cong) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
53 |
|
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
54 |
lemma inner_Basis_INF_left: "i \<in> Basis \<Longrightarrow> (INF x\<in>X. f x) \<bullet> i = (INF x\<in>X. f x \<bullet> i)" |
69260
0a9688695a1b
removed relics of ASCII syntax for indexed big operators
haftmann
parents:
69000
diff
changeset
|
55 |
and inner_Basis_SUP_left: "i \<in> Basis \<Longrightarrow> (SUP x\<in>X. f x) \<bullet> i = (SUP x\<in>X. f x \<bullet> i)" |
69861
62e47f06d22c
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
haftmann
parents:
69730
diff
changeset
|
56 |
using eucl_Sup [of "f ` X"] eucl_Inf [of "f ` X"] by (simp_all add: image_comp) |
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
57 |
|
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
58 |
lemma abs_inner: "i \<in> Basis \<Longrightarrow> \<bar>x\<bar> \<bullet> i = \<bar>x \<bullet> i\<bar>" |
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
59 |
by (auto simp: eucl_abs) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
60 |
|
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
61 |
lemma |
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
62 |
abs_scaleR: "\<bar>a *\<^sub>R b\<bar> = \<bar>a\<bar> *\<^sub>R \<bar>b\<bar>" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
63 |
by (auto simp: eucl_abs abs_mult intro!: euclidean_eqI) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
64 |
|
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
65 |
lemma interval_inner_leI: |
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
66 |
assumes "x \<in> {a .. b}" "0 \<le> i" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
67 |
shows "a\<bullet>i \<le> x\<bullet>i" "x\<bullet>i \<le> b\<bullet>i" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
68 |
using assms |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
69 |
unfolding euclidean_inner[of a i] euclidean_inner[of x i] euclidean_inner[of b i] |
64267 | 70 |
by (auto intro!: ordered_comm_monoid_add_class.sum_mono mult_right_mono simp: eucl_le) |
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
71 |
|
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
72 |
lemma inner_nonneg_nonneg: |
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
73 |
shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a \<bullet> b" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
74 |
using interval_inner_leI[of a 0 a b] |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
75 |
by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
76 |
|
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
77 |
lemma inner_Basis_mono: |
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
78 |
shows "a \<le> b \<Longrightarrow> c \<in> Basis \<Longrightarrow> a \<bullet> c \<le> b \<bullet> c" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
79 |
by (simp add: eucl_le) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
80 |
|
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
81 |
lemma Basis_nonneg[intro, simp]: "i \<in> Basis \<Longrightarrow> 0 \<le> i" |
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
82 |
by (auto simp: eucl_le inner_Basis) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
83 |
|
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
84 |
lemma Sup_eq_maximum_componentwise: |
54781 | 85 |
fixes s::"'a set" |
86 |
assumes i: "\<And>b. b \<in> Basis \<Longrightarrow> X \<bullet> b = i b \<bullet> b" |
|
87 |
assumes sup: "\<And>b x. b \<in> Basis \<Longrightarrow> x \<in> s \<Longrightarrow> x \<bullet> b \<le> X \<bullet> b" |
|
88 |
assumes i_s: "\<And>b. b \<in> Basis \<Longrightarrow> (i b \<bullet> b) \<in> (\<lambda>x. x \<bullet> b) ` s" |
|
89 |
shows "Sup s = X" |
|
90 |
using assms |
|
64267 | 91 |
unfolding eucl_Sup euclidean_representation_sum |
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
61945
diff
changeset
|
92 |
by (auto intro!: conditionally_complete_lattice_class.cSup_eq_maximum) |
54781 | 93 |
|
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
94 |
lemma Inf_eq_minimum_componentwise: |
54781 | 95 |
assumes i: "\<And>b. b \<in> Basis \<Longrightarrow> X \<bullet> b = i b \<bullet> b" |
96 |
assumes sup: "\<And>b x. b \<in> Basis \<Longrightarrow> x \<in> s \<Longrightarrow> X \<bullet> b \<le> x \<bullet> b" |
|
97 |
assumes i_s: "\<And>b. b \<in> Basis \<Longrightarrow> (i b \<bullet> b) \<in> (\<lambda>x. x \<bullet> b) ` s" |
|
98 |
shows "Inf s = X" |
|
99 |
using assms |
|
64267 | 100 |
unfolding eucl_Inf euclidean_representation_sum |
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
61945
diff
changeset
|
101 |
by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum) |
54781 | 102 |
|
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
103 |
end |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
104 |
|
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
105 |
proposition compact_attains_Inf_componentwise: |
54781 | 106 |
fixes b::"'a::ordered_euclidean_space" |
107 |
assumes "b \<in> Basis" assumes "X \<noteq> {}" "compact X" |
|
108 |
obtains x where "x \<in> X" "x \<bullet> b = Inf X \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> x \<bullet> b \<le> y \<bullet> b" |
|
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
109 |
proof atomize_elim |
54781 | 110 |
let ?proj = "(\<lambda>x. x \<bullet> b) ` X" |
111 |
from assms have "compact ?proj" "?proj \<noteq> {}" |
|
56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56190
diff
changeset
|
112 |
by (auto intro!: compact_continuous_image continuous_intros) |
54781 | 113 |
from compact_attains_inf[OF this] |
114 |
obtain s x |
|
115 |
where s: "s\<in>(\<lambda>x. x \<bullet> b) ` X" "\<And>t. t\<in>(\<lambda>x. x \<bullet> b) ` X \<Longrightarrow> s \<le> t" |
|
116 |
and x: "x \<in> X" "s = x \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> x \<bullet> b \<le> y \<bullet> b" |
|
117 |
by auto |
|
118 |
hence "Inf ?proj = x \<bullet> b" |
|
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
61945
diff
changeset
|
119 |
by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum) |
54781 | 120 |
hence "x \<bullet> b = Inf X \<bullet> b" |
64267 | 121 |
by (auto simp: eucl_Inf inner_sum_left inner_Basis if_distrib \<open>b \<in> Basis\<close> sum.delta |
56166 | 122 |
cong: if_cong) |
54781 | 123 |
with x show "\<exists>x. x \<in> X \<and> x \<bullet> b = Inf X \<bullet> b \<and> (\<forall>y. y \<in> X \<longrightarrow> x \<bullet> b \<le> y \<bullet> b)" by blast |
124 |
qed |
|
125 |
||
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
126 |
proposition |
54781 | 127 |
compact_attains_Sup_componentwise: |
128 |
fixes b::"'a::ordered_euclidean_space" |
|
129 |
assumes "b \<in> Basis" assumes "X \<noteq> {}" "compact X" |
|
130 |
obtains x where "x \<in> X" "x \<bullet> b = Sup X \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> y \<bullet> b \<le> x \<bullet> b" |
|
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
131 |
proof atomize_elim |
54781 | 132 |
let ?proj = "(\<lambda>x. x \<bullet> b) ` X" |
133 |
from assms have "compact ?proj" "?proj \<noteq> {}" |
|
56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56190
diff
changeset
|
134 |
by (auto intro!: compact_continuous_image continuous_intros) |
54781 | 135 |
from compact_attains_sup[OF this] |
136 |
obtain s x |
|
137 |
where s: "s\<in>(\<lambda>x. x \<bullet> b) ` X" "\<And>t. t\<in>(\<lambda>x. x \<bullet> b) ` X \<Longrightarrow> t \<le> s" |
|
138 |
and x: "x \<in> X" "s = x \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> y \<bullet> b \<le> x \<bullet> b" |
|
139 |
by auto |
|
140 |
hence "Sup ?proj = x \<bullet> b" |
|
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
61945
diff
changeset
|
141 |
by (auto intro!: cSup_eq_maximum) |
54781 | 142 |
hence "x \<bullet> b = Sup X \<bullet> b" |
64267 | 143 |
by (auto simp: eucl_Sup[where 'a='a] inner_sum_left inner_Basis if_distrib \<open>b \<in> Basis\<close> sum.delta |
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
61945
diff
changeset
|
144 |
cong: if_cong) |
54781 | 145 |
with x show "\<exists>x. x \<in> X \<and> x \<bullet> b = Sup X \<bullet> b \<and> (\<forall>y. y \<in> X \<longrightarrow> y \<bullet> b \<le> x \<bullet> b)" by blast |
146 |
qed |
|
147 |
||
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
148 |
lemma (in order) atLeastatMost_empty'[simp]: |
69508 | 149 |
"(\<not> a \<le> b) \<Longrightarrow> {a..b} = {}" |
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
150 |
by (auto) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
151 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
152 |
instance real :: ordered_euclidean_space |
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
61945
diff
changeset
|
153 |
by standard auto |
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
154 |
|
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
155 |
lemma in_Basis_prod_iff: |
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
156 |
fixes i::"'a::euclidean_space*'b::euclidean_space" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
157 |
shows "i \<in> Basis \<longleftrightarrow> fst i = 0 \<and> snd i \<in> Basis \<or> snd i = 0 \<and> fst i \<in> Basis" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
158 |
by (cases i) (auto simp: Basis_prod_def) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
159 |
|
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
160 |
instantiation%unimportant prod :: (abs, abs) abs |
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
161 |
begin |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
162 |
|
61945 | 163 |
definition "\<bar>x\<bar> = (\<bar>fst x\<bar>, \<bar>snd x\<bar>)" |
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
164 |
|
61945 | 165 |
instance .. |
166 |
||
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
167 |
end |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
168 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
169 |
instance prod :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space |
61169 | 170 |
by standard |
64267 | 171 |
(auto intro!: add_mono simp add: euclidean_representation_sum' Ball_def inner_prod_def |
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
172 |
in_Basis_prod_iff inner_Basis_inf_left inner_Basis_sup_left inner_Basis_INF_left Inf_prod_def |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
173 |
inner_Basis_SUP_left Sup_prod_def less_prod_def less_eq_prod_def eucl_le[where 'a='a] |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
174 |
eucl_le[where 'a='b] abs_prod_def abs_inner) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
175 |
|
61808 | 176 |
text\<open>Instantiation for intervals on \<open>ordered_euclidean_space\<close>\<close> |
56188 | 177 |
|
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
178 |
proposition |
61076 | 179 |
fixes a :: "'a::ordered_euclidean_space" |
56188 | 180 |
shows cbox_interval: "cbox a b = {a..b}" |
181 |
and interval_cbox: "{a..b} = cbox a b" |
|
182 |
and eucl_le_atMost: "{x. \<forall>i\<in>Basis. x \<bullet> i <= a \<bullet> i} = {..a}" |
|
183 |
and eucl_le_atLeast: "{x. \<forall>i\<in>Basis. a \<bullet> i <= x \<bullet> i} = {a..}" |
|
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
184 |
by (auto simp: eucl_le[where 'a='a] eucl_less_def box_def cbox_def) |
56188 | 185 |
|
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
186 |
lemma vec_nth_real_1_iff_cbox [simp]: |
67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67685
diff
changeset
|
187 |
fixes a b :: real |
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67685
diff
changeset
|
188 |
shows "(\<lambda>x::real^1. x $ 1) ` S = {a..b} \<longleftrightarrow> S = cbox (vec a) (vec b)" |
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67685
diff
changeset
|
189 |
by (metis interval_cbox vec_nth_1_iff_cbox) |
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67685
diff
changeset
|
190 |
|
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
191 |
lemma closed_eucl_atLeastAtMost[simp, intro]: |
61076 | 192 |
fixes a :: "'a::ordered_euclidean_space" |
56188 | 193 |
shows "closed {a..b}" |
194 |
by (simp add: cbox_interval[symmetric] closed_cbox) |
|
195 |
||
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
196 |
lemma closed_eucl_atMost[simp, intro]: |
61076 | 197 |
fixes a :: "'a::ordered_euclidean_space" |
56188 | 198 |
shows "closed {..a}" |
66827
c94531b5007d
Divided Topology_Euclidean_Space in two, creating new theory Connected. Also deleted some duplicate / variant theorems
paulson <lp15@cam.ac.uk>
parents:
66453
diff
changeset
|
199 |
by (simp add: closed_interval_left eucl_le_atMost[symmetric]) |
56188 | 200 |
|
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
201 |
lemma closed_eucl_atLeast[simp, intro]: |
61076 | 202 |
fixes a :: "'a::ordered_euclidean_space" |
56188 | 203 |
shows "closed {a..}" |
66827
c94531b5007d
Divided Topology_Euclidean_Space in two, creating new theory Connected. Also deleted some duplicate / variant theorems
paulson <lp15@cam.ac.uk>
parents:
66453
diff
changeset
|
204 |
by (simp add: closed_interval_right eucl_le_atLeast[symmetric]) |
56188 | 205 |
|
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
206 |
lemma bounded_closed_interval [simp]: |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
207 |
fixes a :: "'a::ordered_euclidean_space" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
208 |
shows "bounded {a .. b}" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
209 |
using bounded_cbox[of a b] |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
210 |
by (metis interval_cbox) |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
211 |
|
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
212 |
lemma convex_closed_interval [simp]: |
56190 | 213 |
fixes a :: "'a::ordered_euclidean_space" |
214 |
shows "convex {a .. b}" |
|
215 |
using convex_box[of a b] |
|
216 |
by (metis interval_cbox) |
|
217 |
||
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
218 |
lemma image_smult_interval:"(\<lambda>x. m *\<^sub>R (x::_::ordered_euclidean_space)) ` {a .. b} = |
56188 | 219 |
(if {a .. b} = {} then {} else if 0 \<le> m then {m *\<^sub>R a .. m *\<^sub>R b} else {m *\<^sub>R b .. m *\<^sub>R a})" |
220 |
using image_smult_cbox[of m a b] |
|
221 |
by (simp add: cbox_interval) |
|
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
222 |
|
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
223 |
lemma [simp]: |
67685
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
66827
diff
changeset
|
224 |
fixes a b::"'a::ordered_euclidean_space" and r s::real |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
66827
diff
changeset
|
225 |
shows is_interval_io: "is_interval {..<r}" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
66827
diff
changeset
|
226 |
and is_interval_ic: "is_interval {..a}" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
66827
diff
changeset
|
227 |
and is_interval_oi: "is_interval {r<..}" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
66827
diff
changeset
|
228 |
and is_interval_ci: "is_interval {a..}" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
66827
diff
changeset
|
229 |
and is_interval_oo: "is_interval {r<..<s}" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
66827
diff
changeset
|
230 |
and is_interval_oc: "is_interval {r<..s}" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
66827
diff
changeset
|
231 |
and is_interval_co: "is_interval {r..<s}" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
66827
diff
changeset
|
232 |
and is_interval_cc: "is_interval {b..a}" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
66827
diff
changeset
|
233 |
by (force simp: is_interval_def eucl_le[where 'a='a])+ |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
66827
diff
changeset
|
234 |
|
69000 | 235 |
lemma connected_interval [simp]: |
236 |
fixes a b::"'a::ordered_euclidean_space" |
|
237 |
shows "connected {a..b}" |
|
238 |
using is_interval_cc is_interval_connected by blast |
|
239 |
||
240 |
lemma path_connected_interval [simp]: |
|
241 |
fixes a b::"'a::ordered_euclidean_space" |
|
242 |
shows "path_connected {a..b}" |
|
243 |
using is_interval_cc is_interval_path_connected by blast |
|
244 |
||
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
245 |
lemma is_interval_real_ereal_oo: "is_interval (real_of_ereal ` {N<..<M::ereal})" |
67685
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
66827
diff
changeset
|
246 |
by (auto simp: real_atLeastGreaterThan_eq) |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
247 |
|
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
248 |
lemma compact_interval [simp]: |
56190 | 249 |
fixes a b::"'a::ordered_euclidean_space" |
250 |
shows "compact {a .. b}" |
|
251 |
by (metis compact_cbox interval_cbox) |
|
252 |
||
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
253 |
lemma homeomorphic_closed_intervals: |
62620
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62376
diff
changeset
|
254 |
fixes a :: "'a::euclidean_space" and b and c :: "'a::euclidean_space" and d |
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62376
diff
changeset
|
255 |
assumes "box a b \<noteq> {}" and "box c d \<noteq> {}" |
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62376
diff
changeset
|
256 |
shows "(cbox a b) homeomorphic (cbox c d)" |
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62376
diff
changeset
|
257 |
apply (rule homeomorphic_convex_compact) |
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62376
diff
changeset
|
258 |
using assms apply auto |
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62376
diff
changeset
|
259 |
done |
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62376
diff
changeset
|
260 |
|
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
261 |
lemma homeomorphic_closed_intervals_real: |
62620
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62376
diff
changeset
|
262 |
fixes a::real and b and c::real and d |
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62376
diff
changeset
|
263 |
assumes "a<b" and "c<d" |
68239 | 264 |
shows "{a..b} homeomorphic {c..d}" |
265 |
using assms by (auto intro: homeomorphic_convex_compact) |
|
62620
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62376
diff
changeset
|
266 |
|
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
267 |
no_notation |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
268 |
eucl_less (infix "<e" 50) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
269 |
|
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
270 |
lemma One_nonneg: "0 \<le> (\<Sum>Basis::'a::ordered_euclidean_space)" |
64267 | 271 |
by (auto intro: sum_nonneg) |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
272 |
|
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
273 |
lemma |
56190 | 274 |
fixes a b::"'a::ordered_euclidean_space" |
275 |
shows bdd_above_cbox[intro, simp]: "bdd_above (cbox a b)" |
|
276 |
and bdd_below_cbox[intro, simp]: "bdd_below (cbox a b)" |
|
277 |
and bdd_above_box[intro, simp]: "bdd_above (box a b)" |
|
278 |
and bdd_below_box[intro, simp]: "bdd_below (box a b)" |
|
279 |
unfolding atomize_conj |
|
280 |
by (metis bdd_above_Icc bdd_above_mono bdd_below_Icc bdd_below_mono bounded_box |
|
68120 | 281 |
bounded_subset_cbox_symmetric interval_cbox) |
56190 | 282 |
|
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
283 |
instantiation vec :: (ordered_euclidean_space, finite) ordered_euclidean_space |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
284 |
begin |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
285 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68239
diff
changeset
|
286 |
definition%important "inf x y = (\<chi> i. inf (x $ i) (y $ i))" |
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68239
diff
changeset
|
287 |
definition%important "sup x y = (\<chi> i. sup (x $ i) (y $ i))" |
69260
0a9688695a1b
removed relics of ASCII syntax for indexed big operators
haftmann
parents:
69000
diff
changeset
|
288 |
definition%important "Inf X = (\<chi> i. (INF x\<in>X. x $ i))" |
0a9688695a1b
removed relics of ASCII syntax for indexed big operators
haftmann
parents:
69000
diff
changeset
|
289 |
definition%important "Sup X = (\<chi> i. (SUP x\<in>X. x $ i))" |
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68239
diff
changeset
|
290 |
definition%important "\<bar>x\<bar> = (\<chi> i. \<bar>x $ i\<bar>)" |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
291 |
|
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
292 |
instance |
61169 | 293 |
apply standard |
64267 | 294 |
unfolding euclidean_representation_sum' |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
295 |
apply (auto simp: less_eq_vec_def inf_vec_def sup_vec_def Inf_vec_def Sup_vec_def inner_axis |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
296 |
Basis_vec_def inner_Basis_inf_left inner_Basis_sup_left inner_Basis_INF_left |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
297 |
inner_Basis_SUP_left eucl_le[where 'a='a] less_le_not_le abs_vec_def abs_inner) |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
298 |
done |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
299 |
|
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
300 |
end |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
301 |
|
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
302 |
lemma ANR_interval [iff]: |
63469
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
62620
diff
changeset
|
303 |
fixes a :: "'a::ordered_euclidean_space" |
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
62620
diff
changeset
|
304 |
shows "ANR{a..b}" |
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
62620
diff
changeset
|
305 |
by (simp add: interval_cbox) |
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
62620
diff
changeset
|
306 |
|
69730
0c3dcb3a17f6
tagged 5 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
307 |
lemma ENR_interval [iff]: |
63469
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
62620
diff
changeset
|
308 |
fixes a :: "'a::ordered_euclidean_space" |
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
62620
diff
changeset
|
309 |
shows "ENR{a..b}" |
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
62620
diff
changeset
|
310 |
by (auto simp: interval_cbox) |
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
62620
diff
changeset
|
311 |
|
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
312 |
end |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
313 |