author  immler 
Tue, 18 Mar 2014 10:12:58 +0100  
changeset 56189  c4daa97ac57a 
parent 56188  0268784f60da 
child 56290  801a72ad52d3 
permissions  rwrr 
33714
eb2574ac4173
Added new lemmas to Euclidean Space by Robert Himmelmann
hoelzl
parents:
33324
diff
changeset

1 
(* title: HOL/Library/Topology_Euclidian_Space.thy 
33175  2 
Author: Amine Chaieb, University of Cambridge 
3 
Author: Robert Himmelmann, TU Muenchen 

44075  4 
Author: Brian Huffman, Portland State University 
33175  5 
*) 
6 

7 
header {* Elementary topology in Euclidean space. *} 

8 

9 
theory Topology_Euclidean_Space 

50087  10 
imports 
50938  11 
Complex_Main 
50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

12 
"~~/src/HOL/Library/Countable_Set" 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

13 
"~~/src/HOL/Library/FuncSet" 
50938  14 
Linear_Algebra 
50087  15 
Norm_Arith 
16 
begin 

17 

50972  18 
lemma dist_0_norm: 
19 
fixes x :: "'a::real_normed_vector" 

20 
shows "dist 0 x = norm x" 

21 
unfolding dist_norm by simp 

22 

50943
88a00a1c7c2c
use accumulation point characterization (avoids t1_space restriction for equivalence of countable and sequential compactness); remove heine_borel_lemma
hoelzl
parents:
50942
diff
changeset

23 
lemma dist_double: "dist x y < d / 2 \<Longrightarrow> dist x z < d / 2 \<Longrightarrow> dist y z < d" 
88a00a1c7c2c
use accumulation point characterization (avoids t1_space restriction for equivalence of countable and sequential compactness); remove heine_borel_lemma
hoelzl
parents:
50942
diff
changeset

24 
using dist_triangle[of y z x] by (simp add: dist_commute) 
88a00a1c7c2c
use accumulation point characterization (avoids t1_space restriction for equivalence of countable and sequential compactness); remove heine_borel_lemma
hoelzl
parents:
50942
diff
changeset

25 

50972  26 
(* LEGACY *) 
53640  27 
lemma lim_subseq: "subseq r \<Longrightarrow> s > l \<Longrightarrow> (s \<circ> r) > l" 
50972  28 
by (rule LIMSEQ_subseq_LIMSEQ) 
29 

53282  30 
lemma countable_PiE: 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

31 
"finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (PiE I F)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

32 
by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

33 

51481
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset

34 
lemma Lim_within_open: 
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset

35 
fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space" 
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset

36 
shows "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f > l)(at a within S) \<longleftrightarrow> (f > l)(at a)" 
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset

37 
by (fact tendsto_within_open) 
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset

38 

ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset

39 
lemma continuous_on_union: 
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset

40 
"closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f" 
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset

41 
by (fact continuous_on_closed_Un) 
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset

42 

ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset

43 
lemma continuous_on_cases: 
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset

44 
"closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t g \<Longrightarrow> 
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset

45 
\<forall>x. (x\<in>s \<and> \<not> P x) \<or> (x \<in> t \<and> P x) \<longrightarrow> f x = g x \<Longrightarrow> 
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset

46 
continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)" 
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset

47 
by (rule continuous_on_If) auto 
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset

48 

53255  49 

50087  50 
subsection {* Topological Basis *} 
51 

52 
context topological_space 

53 
begin 

54 

53291  55 
definition "topological_basis B \<longleftrightarrow> 
56 
(\<forall>b\<in>B. open b) \<and> (\<forall>x. open x \<longrightarrow> (\<exists>B'. B' \<subseteq> B \<and> \<Union>B' = x))" 

51343
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

57 

b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

58 
lemma topological_basis: 
53291  59 
"topological_basis B \<longleftrightarrow> (\<forall>x. open x \<longleftrightarrow> (\<exists>B'. B' \<subseteq> B \<and> \<Union>B' = x))" 
50998  60 
unfolding topological_basis_def 
61 
apply safe 

62 
apply fastforce 

63 
apply fastforce 

64 
apply (erule_tac x="x" in allE) 

65 
apply simp 

66 
apply (rule_tac x="{x}" in exI) 

67 
apply auto 

68 
done 

69 

50087  70 
lemma topological_basis_iff: 
71 
assumes "\<And>B'. B' \<in> B \<Longrightarrow> open B'" 

72 
shows "topological_basis B \<longleftrightarrow> (\<forall>O'. open O' \<longrightarrow> (\<forall>x\<in>O'. \<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'))" 

73 
(is "_ \<longleftrightarrow> ?rhs") 

74 
proof safe 

75 
fix O' and x::'a 

76 
assume H: "topological_basis B" "open O'" "x \<in> O'" 

53282  77 
then have "(\<exists>B'\<subseteq>B. \<Union>B' = O')" by (simp add: topological_basis_def) 
50087  78 
then obtain B' where "B' \<subseteq> B" "O' = \<Union>B'" by auto 
53282  79 
then show "\<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'" using H by auto 
50087  80 
next 
81 
assume H: ?rhs 

53282  82 
show "topological_basis B" 
83 
using assms unfolding topological_basis_def 

50087  84 
proof safe 
53640  85 
fix O' :: "'a set" 
53282  86 
assume "open O'" 
50087  87 
with H obtain f where "\<forall>x\<in>O'. f x \<in> B \<and> x \<in> f x \<and> f x \<subseteq> O'" 
88 
by (force intro: bchoice simp: Bex_def) 

53282  89 
then show "\<exists>B'\<subseteq>B. \<Union>B' = O'" 
50087  90 
by (auto intro: exI[where x="{f x x. x \<in> O'}"]) 
91 
qed 

92 
qed 

93 

94 
lemma topological_basisI: 

95 
assumes "\<And>B'. B' \<in> B \<Longrightarrow> open B'" 

53282  96 
and "\<And>O' x. open O' \<Longrightarrow> x \<in> O' \<Longrightarrow> \<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'" 
50087  97 
shows "topological_basis B" 
98 
using assms by (subst topological_basis_iff) auto 

99 

100 
lemma topological_basisE: 

101 
fixes O' 

102 
assumes "topological_basis B" 

53282  103 
and "open O'" 
104 
and "x \<in> O'" 

50087  105 
obtains B' where "B' \<in> B" "x \<in> B'" "B' \<subseteq> O'" 
106 
proof atomize_elim 

53282  107 
from assms have "\<And>B'. B'\<in>B \<Longrightarrow> open B'" 
108 
by (simp add: topological_basis_def) 

50087  109 
with topological_basis_iff assms 
53282  110 
show "\<exists>B'. B' \<in> B \<and> x \<in> B' \<and> B' \<subseteq> O'" 
111 
using assms by (simp add: Bex_def) 

50087  112 
qed 
113 

50094
84ddcf5364b4
allow arbitrary enumerations of basis in locale for generation of borel sets
immler
parents:
50087
diff
changeset

114 
lemma topological_basis_open: 
84ddcf5364b4
allow arbitrary enumerations of basis in locale for generation of borel sets
immler
parents:
50087
diff
changeset

115 
assumes "topological_basis B" 
53282  116 
and "X \<in> B" 
50094
84ddcf5364b4
allow arbitrary enumerations of basis in locale for generation of borel sets
immler
parents:
50087
diff
changeset

117 
shows "open X" 
53282  118 
using assms by (simp add: topological_basis_def) 
50094
84ddcf5364b4
allow arbitrary enumerations of basis in locale for generation of borel sets
immler
parents:
50087
diff
changeset

119 

51343
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

120 
lemma topological_basis_imp_subbasis: 
53255  121 
assumes B: "topological_basis B" 
122 
shows "open = generate_topology B" 

51343
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

123 
proof (intro ext iffI) 
53255  124 
fix S :: "'a set" 
125 
assume "open S" 

51343
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

126 
with B obtain B' where "B' \<subseteq> B" "S = \<Union>B'" 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

127 
unfolding topological_basis_def by blast 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

128 
then show "generate_topology B S" 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

129 
by (auto intro: generate_topology.intros dest: topological_basis_open) 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

130 
next 
53255  131 
fix S :: "'a set" 
132 
assume "generate_topology B S" 

133 
then show "open S" 

51343
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

134 
by induct (auto dest: topological_basis_open[OF B]) 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

135 
qed 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

136 

50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

137 
lemma basis_dense: 
53640  138 
fixes B :: "'a set set" 
139 
and f :: "'a set \<Rightarrow> 'a" 

50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

140 
assumes "topological_basis B" 
53255  141 
and choosefrom_basis: "\<And>B'. B' \<noteq> {} \<Longrightarrow> f B' \<in> B'" 
55522  142 
shows "\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>B' \<in> B. f B' \<in> X)" 
50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

143 
proof (intro allI impI) 
53640  144 
fix X :: "'a set" 
145 
assume "open X" and "X \<noteq> {}" 

50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

146 
from topological_basisE[OF `topological_basis B` `open X` choosefrom_basis[OF `X \<noteq> {}`]] 
55522  147 
obtain B' where "B' \<in> B" "f X \<in> B'" "B' \<subseteq> X" . 
53255  148 
then show "\<exists>B'\<in>B. f B' \<in> X" 
149 
by (auto intro!: choosefrom_basis) 

50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

150 
qed 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

151 

50087  152 
end 
153 

50882
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

154 
lemma topological_basis_prod: 
53255  155 
assumes A: "topological_basis A" 
156 
and B: "topological_basis B" 

50882
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

157 
shows "topological_basis ((\<lambda>(a, b). a \<times> b) ` (A \<times> B))" 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

158 
unfolding topological_basis_def 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

159 
proof (safe, simp_all del: ex_simps add: subset_image_iff ex_simps(1)[symmetric]) 
53255  160 
fix S :: "('a \<times> 'b) set" 
161 
assume "open S" 

50882
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

162 
then show "\<exists>X\<subseteq>A \<times> B. (\<Union>(a,b)\<in>X. a \<times> b) = S" 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

163 
proof (safe intro!: exI[of _ "{x\<in>A \<times> B. fst x \<times> snd x \<subseteq> S}"]) 
53255  164 
fix x y 
165 
assume "(x, y) \<in> S" 

50882
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

166 
from open_prod_elim[OF `open S` this] 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

167 
obtain a b where a: "open a""x \<in> a" and b: "open b" "y \<in> b" and "a \<times> b \<subseteq> S" 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

168 
by (metis mem_Sigma_iff) 
55522  169 
moreover 
170 
from A a obtain A0 where "A0 \<in> A" "x \<in> A0" "A0 \<subseteq> a" 

171 
by (rule topological_basisE) 

172 
moreover 

173 
from B b obtain B0 where "B0 \<in> B" "y \<in> B0" "B0 \<subseteq> b" 

174 
by (rule topological_basisE) 

50882
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

175 
ultimately show "(x, y) \<in> (\<Union>(a, b)\<in>{X \<in> A \<times> B. fst X \<times> snd X \<subseteq> S}. a \<times> b)" 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

176 
by (intro UN_I[of "(A0, B0)"]) auto 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

177 
qed auto 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

178 
qed (metis A B topological_basis_open open_Times) 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

179 

53255  180 

50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

181 
subsection {* Countable Basis *} 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

182 

dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

183 
locale countable_basis = 
53640  184 
fixes B :: "'a::topological_space set set" 
50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

185 
assumes is_basis: "topological_basis B" 
53282  186 
and countable_basis: "countable B" 
33175  187 
begin 
188 

50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

189 
lemma open_countable_basis_ex: 
50087  190 
assumes "open X" 
50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

191 
shows "\<exists>B' \<subseteq> B. X = Union B'" 
53255  192 
using assms countable_basis is_basis 
193 
unfolding topological_basis_def by blast 

50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

194 

dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

195 
lemma open_countable_basisE: 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

196 
assumes "open X" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

197 
obtains B' where "B' \<subseteq> B" "X = Union B'" 
53255  198 
using assms open_countable_basis_ex 
199 
by (atomize_elim) simp 

50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

200 

dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

201 
lemma countable_dense_exists: 
53291  202 
"\<exists>D::'a set. countable D \<and> (\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>d \<in> D. d \<in> X))" 
50087  203 
proof  
50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

204 
let ?f = "(\<lambda>B'. SOME x. x \<in> B')" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

205 
have "countable (?f ` B)" using countable_basis by simp 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

206 
with basis_dense[OF is_basis, of ?f] show ?thesis 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

207 
by (intro exI[where x="?f ` B"]) (metis (mono_tags) all_not_in_conv imageI someI) 
50087  208 
qed 
209 

210 
lemma countable_dense_setE: 

50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

211 
obtains D :: "'a set" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

212 
where "countable D" "\<And>X. open X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> \<exists>d \<in> D. d \<in> X" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

213 
using countable_dense_exists by blast 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

214 

50087  215 
end 
216 

50883  217 
lemma (in first_countable_topology) first_countable_basisE: 
218 
obtains A where "countable A" "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a" 

219 
"\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)" 

220 
using first_countable_basis[of x] 

51473  221 
apply atomize_elim 
222 
apply (elim exE) 

223 
apply (rule_tac x="range A" in exI) 

224 
apply auto 

225 
done 

50883  226 

51105  227 
lemma (in first_countable_topology) first_countable_basis_Int_stableE: 
228 
obtains A where "countable A" "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a" 

229 
"\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)" 

230 
"\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<inter> b \<in> A" 

231 
proof atomize_elim 

55522  232 
obtain A' where A': 
233 
"countable A'" 

234 
"\<And>a. a \<in> A' \<Longrightarrow> x \<in> a" 

235 
"\<And>a. a \<in> A' \<Longrightarrow> open a" 

236 
"\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>a\<in>A'. a \<subseteq> S" 

237 
by (rule first_countable_basisE) blast 

51105  238 
def A \<equiv> "(\<lambda>N. \<Inter>((\<lambda>n. from_nat_into A' n) ` N)) ` (Collect finite::nat set set)" 
53255  239 
then show "\<exists>A. countable A \<and> (\<forall>a. a \<in> A \<longrightarrow> x \<in> a) \<and> (\<forall>a. a \<in> A \<longrightarrow> open a) \<and> 
51105  240 
(\<forall>S. open S \<longrightarrow> x \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)) \<and> (\<forall>a b. a \<in> A \<longrightarrow> b \<in> A \<longrightarrow> a \<inter> b \<in> A)" 
241 
proof (safe intro!: exI[where x=A]) 

53255  242 
show "countable A" 
243 
unfolding A_def by (intro countable_image countable_Collect_finite) 

244 
fix a 

245 
assume "a \<in> A" 

246 
then show "x \<in> a" "open a" 

247 
using A'(4)[OF open_UNIV] by (auto simp: A_def intro: A' from_nat_into) 

51105  248 
next 
52141
eff000cab70f
weaker precendence of syntax for big intersection and union on sets
haftmann
parents:
51773
diff
changeset

249 
let ?int = "\<lambda>N. \<Inter>(from_nat_into A' ` N)" 
53255  250 
fix a b 
251 
assume "a \<in> A" "b \<in> A" 

252 
then obtain N M where "a = ?int N" "b = ?int M" "finite (N \<union> M)" 

253 
by (auto simp: A_def) 

254 
then show "a \<inter> b \<in> A" 

255 
by (auto simp: A_def intro!: image_eqI[where x="N \<union> M"]) 

51105  256 
next 
53255  257 
fix S 
258 
assume "open S" "x \<in> S" 

259 
then obtain a where a: "a\<in>A'" "a \<subseteq> S" using A' by blast 

260 
then show "\<exists>a\<in>A. a \<subseteq> S" using a A' 

51105  261 
by (intro bexI[where x=a]) (auto simp: A_def intro: image_eqI[where x="{to_nat_on A' a}"]) 
262 
qed 

263 
qed 

264 

51473  265 
lemma (in topological_space) first_countableI: 
53255  266 
assumes "countable A" 
267 
and 1: "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a" 

268 
and 2: "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>a\<in>A. a \<subseteq> S" 

51473  269 
shows "\<exists>A::nat \<Rightarrow> 'a set. (\<forall>i. x \<in> A i \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))" 
270 
proof (safe intro!: exI[of _ "from_nat_into A"]) 

53255  271 
fix i 
51473  272 
have "A \<noteq> {}" using 2[of UNIV] by auto 
53255  273 
show "x \<in> from_nat_into A i" "open (from_nat_into A i)" 
274 
using range_from_nat_into_subset[OF `A \<noteq> {}`] 1 by auto 

275 
next 

276 
fix S 

277 
assume "open S" "x\<in>S" from 2[OF this] 

278 
show "\<exists>i. from_nat_into A i \<subseteq> S" 

279 
using subset_range_from_nat_into[OF `countable A`] by auto 

51473  280 
qed 
51350  281 

50883  282 
instance prod :: (first_countable_topology, first_countable_topology) first_countable_topology 
283 
proof 

284 
fix x :: "'a \<times> 'b" 

55522  285 
obtain A where A: 
286 
"countable A" 

287 
"\<And>a. a \<in> A \<Longrightarrow> fst x \<in> a" 

288 
"\<And>a. a \<in> A \<Longrightarrow> open a" 

289 
"\<And>S. open S \<Longrightarrow> fst x \<in> S \<Longrightarrow> \<exists>a\<in>A. a \<subseteq> S" 

290 
by (rule first_countable_basisE[of "fst x"]) blast 

291 
obtain B where B: 

292 
"countable B" 

293 
"\<And>a. a \<in> B \<Longrightarrow> snd x \<in> a" 

294 
"\<And>a. a \<in> B \<Longrightarrow> open a" 

295 
"\<And>S. open S \<Longrightarrow> snd x \<in> S \<Longrightarrow> \<exists>a\<in>B. a \<subseteq> S" 

296 
by (rule first_countable_basisE[of "snd x"]) blast 

53282  297 
show "\<exists>A::nat \<Rightarrow> ('a \<times> 'b) set. 
298 
(\<forall>i. x \<in> A i \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))" 

51473  299 
proof (rule first_countableI[of "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"], safe) 
53255  300 
fix a b 
301 
assume x: "a \<in> A" "b \<in> B" 

53640  302 
with A(2, 3)[of a] B(2, 3)[of b] show "x \<in> a \<times> b" and "open (a \<times> b)" 
303 
unfolding mem_Times_iff 

304 
by (auto intro: open_Times) 

50883  305 
next 
53255  306 
fix S 
307 
assume "open S" "x \<in> S" 

55522  308 
then obtain a' b' where a'b': "open a'" "open b'" "x \<in> a' \<times> b'" "a' \<times> b' \<subseteq> S" 
309 
by (rule open_prod_elim) 

310 
moreover 

311 
from a'b' A(4)[of a'] B(4)[of b'] 

312 
obtain a b where "a \<in> A" "a \<subseteq> a'" "b \<in> B" "b \<subseteq> b'" 

313 
by auto 

314 
ultimately 

315 
show "\<exists>a\<in>(\<lambda>(a, b). a \<times> b) ` (A \<times> B). a \<subseteq> S" 

50883  316 
by (auto intro!: bexI[of _ "a \<times> b"] bexI[of _ a] bexI[of _ b]) 
317 
qed (simp add: A B) 

318 
qed 

319 

50881
ae630bab13da
renamed countable_basis_space to second_countable_topology
hoelzl
parents:
50526
diff
changeset

320 
class second_countable_topology = topological_space + 
53282  321 
assumes ex_countable_subbasis: 
322 
"\<exists>B::'a::topological_space set set. countable B \<and> open = generate_topology B" 

51343
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

323 
begin 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

324 

b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

325 
lemma ex_countable_basis: "\<exists>B::'a set set. countable B \<and> topological_basis B" 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

326 
proof  
53255  327 
from ex_countable_subbasis obtain B where B: "countable B" "open = generate_topology B" 
328 
by blast 

51343
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

329 
let ?B = "Inter ` {b. finite b \<and> b \<subseteq> B }" 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

330 

b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

331 
show ?thesis 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

332 
proof (intro exI conjI) 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

333 
show "countable ?B" 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

334 
by (intro countable_image countable_Collect_finite_subset B) 
53255  335 
{ 
336 
fix S 

337 
assume "open S" 

51343
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

338 
then have "\<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. (\<Union>b\<in>B'. \<Inter>b) = S" 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

339 
unfolding B 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

340 
proof induct 
53255  341 
case UNIV 
342 
show ?case by (intro exI[of _ "{{}}"]) simp 

51343
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

343 
next 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

344 
case (Int a b) 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

345 
then obtain x y where x: "a = UNION x Inter" "\<And>i. i \<in> x \<Longrightarrow> finite i \<and> i \<subseteq> B" 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

346 
and y: "b = UNION y Inter" "\<And>i. i \<in> y \<Longrightarrow> finite i \<and> i \<subseteq> B" 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

347 
by blast 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

348 
show ?case 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

349 
unfolding x y Int_UN_distrib2 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

350 
by (intro exI[of _ "{i \<union> j i j. i \<in> x \<and> j \<in> y}"]) (auto dest: x(2) y(2)) 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

351 
next 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

352 
case (UN K) 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

353 
then have "\<forall>k\<in>K. \<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. UNION B' Inter = k" by auto 
55522  354 
then obtain k where 
355 
"\<forall>ka\<in>K. k ka \<subseteq> {b. finite b \<and> b \<subseteq> B} \<and> UNION (k ka) Inter = ka" 

356 
unfolding bchoice_iff .. 

51343
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

357 
then show "\<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. UNION B' Inter = \<Union>K" 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

358 
by (intro exI[of _ "UNION K k"]) auto 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

359 
next 
53255  360 
case (Basis S) 
361 
then show ?case 

51343
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

362 
by (intro exI[of _ "{{S}}"]) auto 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

363 
qed 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

364 
then have "(\<exists>B'\<subseteq>Inter ` {b. finite b \<and> b \<subseteq> B}. \<Union>B' = S)" 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

365 
unfolding subset_image_iff by blast } 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

366 
then show "topological_basis ?B" 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

367 
unfolding topological_space_class.topological_basis_def 
53282  368 
by (safe intro!: topological_space_class.open_Inter) 
51343
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

369 
(simp_all add: B generate_topology.Basis subset_eq) 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

370 
qed 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

371 
qed 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

372 

b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

373 
end 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

374 

b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

375 
sublocale second_countable_topology < 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

376 
countable_basis "SOME B. countable B \<and> topological_basis B" 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

377 
using someI_ex[OF ex_countable_basis] 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

378 
by unfold_locales safe 
50094
84ddcf5364b4
allow arbitrary enumerations of basis in locale for generation of borel sets
immler
parents:
50087
diff
changeset

379 

50882
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

380 
instance prod :: (second_countable_topology, second_countable_topology) second_countable_topology 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

381 
proof 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

382 
obtain A :: "'a set set" where "countable A" "topological_basis A" 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

383 
using ex_countable_basis by auto 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

384 
moreover 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

385 
obtain B :: "'b set set" where "countable B" "topological_basis B" 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

386 
using ex_countable_basis by auto 
51343
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

387 
ultimately show "\<exists>B::('a \<times> 'b) set set. countable B \<and> open = generate_topology B" 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

388 
by (auto intro!: exI[of _ "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"] topological_basis_prod 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

389 
topological_basis_imp_subbasis) 
50882
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

390 
qed 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

391 

50883  392 
instance second_countable_topology \<subseteq> first_countable_topology 
393 
proof 

394 
fix x :: 'a 

395 
def B \<equiv> "SOME B::'a set set. countable B \<and> topological_basis B" 

396 
then have B: "countable B" "topological_basis B" 

397 
using countable_basis is_basis 

398 
by (auto simp: countable_basis is_basis) 

53282  399 
then show "\<exists>A::nat \<Rightarrow> 'a set. 
400 
(\<forall>i. x \<in> A i \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))" 

51473  401 
by (intro first_countableI[of "{b\<in>B. x \<in> b}"]) 
402 
(fastforce simp: topological_space_class.topological_basis_def)+ 

50883  403 
qed 
404 

53255  405 

50087  406 
subsection {* Polish spaces *} 
407 

408 
text {* Textbooks define Polish spaces as completely metrizable. 

409 
We assume the topology to be complete for a given metric. *} 

410 

50881
ae630bab13da
renamed countable_basis_space to second_countable_topology
hoelzl
parents:
50526
diff
changeset

411 
class polish_space = complete_space + second_countable_topology 
50087  412 

44517  413 
subsection {* General notion of a topology as a value *} 
33175  414 

53255  415 
definition "istopology L \<longleftrightarrow> 
416 
L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union> K))" 

417 

49834  418 
typedef 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}" 
33175  419 
morphisms "openin" "topology" 
420 
unfolding istopology_def by blast 

421 

422 
lemma istopology_open_in[intro]: "istopology(openin U)" 

423 
using openin[of U] by blast 

424 

425 
lemma topology_inverse': "istopology U \<Longrightarrow> openin (topology U) = U" 

44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

426 
using topology_inverse[unfolded mem_Collect_eq] . 
33175  427 

428 
lemma topology_inverse_iff: "istopology U \<longleftrightarrow> openin (topology U) = U" 

429 
using topology_inverse[of U] istopology_open_in[of "topology U"] by auto 

430 

431 
lemma topology_eq: "T1 = T2 \<longleftrightarrow> (\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S)" 

53255  432 
proof 
433 
assume "T1 = T2" 

434 
then show "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S" by simp 

435 
next 

436 
assume H: "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S" 

437 
then have "openin T1 = openin T2" by (simp add: fun_eq_iff) 

438 
then have "topology (openin T1) = topology (openin T2)" by simp 

439 
then show "T1 = T2" unfolding openin_inverse . 

33175  440 
qed 
441 

442 
text{* Infer the "universe" from union of all sets in the topology. *} 

443 

53640  444 
definition "topspace T = \<Union>{S. openin T S}" 
33175  445 

44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

446 
subsubsection {* Main properties of open sets *} 
33175  447 

448 
lemma openin_clauses: 

449 
fixes U :: "'a topology" 

53282  450 
shows 
451 
"openin U {}" 

452 
"\<And>S T. openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S\<inter>T)" 

453 
"\<And>K. (\<forall>S \<in> K. openin U S) \<Longrightarrow> openin U (\<Union>K)" 

454 
using openin[of U] unfolding istopology_def mem_Collect_eq by fast+ 

33175  455 

456 
lemma openin_subset[intro]: "openin U S \<Longrightarrow> S \<subseteq> topspace U" 

457 
unfolding topspace_def by blast 

53255  458 

459 
lemma openin_empty[simp]: "openin U {}" 

460 
by (simp add: openin_clauses) 

33175  461 

462 
lemma openin_Int[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<inter> T)" 

36362
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
36360
diff
changeset

463 
using openin_clauses by simp 
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
36360
diff
changeset

464 

06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
36360
diff
changeset

465 
lemma openin_Union[intro]: "(\<forall>S \<in>K. openin U S) \<Longrightarrow> openin U (\<Union> K)" 
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
36360
diff
changeset

466 
using openin_clauses by simp 
33175  467 

468 
lemma openin_Un[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<union> T)" 

469 
using openin_Union[of "{S,T}" U] by auto 

470 

53255  471 
lemma openin_topspace[intro, simp]: "openin U (topspace U)" 
472 
by (simp add: openin_Union topspace_def) 

33175  473 

49711  474 
lemma openin_subopen: "openin U S \<longleftrightarrow> (\<forall>x \<in> S. \<exists>T. openin U T \<and> x \<in> T \<and> T \<subseteq> S)" 
475 
(is "?lhs \<longleftrightarrow> ?rhs") 

36584  476 
proof 
49711  477 
assume ?lhs 
478 
then show ?rhs by auto 

36584  479 
next 
480 
assume H: ?rhs 

481 
let ?t = "\<Union>{T. openin U T \<and> T \<subseteq> S}" 

482 
have "openin U ?t" by (simp add: openin_Union) 

483 
also have "?t = S" using H by auto 

484 
finally show "openin U S" . 

33175  485 
qed 
486 

49711  487 

44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

488 
subsubsection {* Closed sets *} 
33175  489 

490 
definition "closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U  S)" 

491 

53255  492 
lemma closedin_subset: "closedin U S \<Longrightarrow> S \<subseteq> topspace U" 
493 
by (metis closedin_def) 

494 

495 
lemma closedin_empty[simp]: "closedin U {}" 

496 
by (simp add: closedin_def) 

497 

498 
lemma closedin_topspace[intro, simp]: "closedin U (topspace U)" 

499 
by (simp add: closedin_def) 

500 

33175  501 
lemma closedin_Un[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<union> T)" 
502 
by (auto simp add: Diff_Un closedin_def) 

503 

53255  504 
lemma Diff_Inter[intro]: "A  \<Inter>S = \<Union> {A  ss. s\<in>S}" 
505 
by auto 

506 

507 
lemma closedin_Inter[intro]: 

508 
assumes Ke: "K \<noteq> {}" 

509 
and Kc: "\<forall>S \<in>K. closedin U S" 

510 
shows "closedin U (\<Inter> K)" 

511 
using Ke Kc unfolding closedin_def Diff_Inter by auto 

33175  512 

513 
lemma closedin_Int[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<inter> T)" 

514 
using closedin_Inter[of "{S,T}" U] by auto 

515 

53255  516 
lemma Diff_Diff_Int: "A  (A  B) = A \<inter> B" 
517 
by blast 

518 

33175  519 
lemma openin_closedin_eq: "openin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> closedin U (topspace U  S)" 
520 
apply (auto simp add: closedin_def Diff_Diff_Int inf_absorb2) 

521 
apply (metis openin_subset subset_eq) 

522 
done 

523 

53255  524 
lemma openin_closedin: "S \<subseteq> topspace U \<Longrightarrow> (openin U S \<longleftrightarrow> closedin U (topspace U  S))" 
33175  525 
by (simp add: openin_closedin_eq) 
526 

53255  527 
lemma openin_diff[intro]: 
528 
assumes oS: "openin U S" 

529 
and cT: "closedin U T" 

530 
shows "openin U (S  T)" 

531 
proof  

33175  532 
have "S  T = S \<inter> (topspace U  T)" using openin_subset[of U S] oS cT 
533 
by (auto simp add: topspace_def openin_subset) 

53282  534 
then show ?thesis using oS cT 
535 
by (auto simp add: closedin_def) 

33175  536 
qed 
537 

53255  538 
lemma closedin_diff[intro]: 
539 
assumes oS: "closedin U S" 

540 
and cT: "openin U T" 

541 
shows "closedin U (S  T)" 

542 
proof  

543 
have "S  T = S \<inter> (topspace U  T)" 

53282  544 
using closedin_subset[of U S] oS cT by (auto simp add: topspace_def) 
53255  545 
then show ?thesis 
546 
using oS cT by (auto simp add: openin_closedin_eq) 

547 
qed 

548 

33175  549 

44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

550 
subsubsection {* Subspace topology *} 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

551 

510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

552 
definition "subtopology U V = topology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)" 
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

553 

510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

554 
lemma istopology_subtopology: "istopology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)" 
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

555 
(is "istopology ?L") 
53255  556 
proof  
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

557 
have "?L {}" by blast 
53255  558 
{ 
559 
fix A B 

560 
assume A: "?L A" and B: "?L B" 

561 
from A B obtain Sa and Sb where Sa: "openin U Sa" "A = Sa \<inter> V" and Sb: "openin U Sb" "B = Sb \<inter> V" 

562 
by blast 

563 
have "A \<inter> B = (Sa \<inter> Sb) \<inter> V" "openin U (Sa \<inter> Sb)" 

564 
using Sa Sb by blast+ 

565 
then have "?L (A \<inter> B)" by blast 

566 
} 

33175  567 
moreover 
53255  568 
{ 
53282  569 
fix K 
570 
assume K: "K \<subseteq> Collect ?L" 

44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

571 
have th0: "Collect ?L = (\<lambda>S. S \<inter> V) ` Collect (openin U)" 
55775  572 
by blast 
33175  573 
from K[unfolded th0 subset_image_iff] 
53255  574 
obtain Sk where Sk: "Sk \<subseteq> Collect (openin U)" "K = (\<lambda>S. S \<inter> V) ` Sk" 
575 
by blast 

576 
have "\<Union>K = (\<Union>Sk) \<inter> V" 

577 
using Sk by auto 

578 
moreover have "openin U (\<Union> Sk)" 

579 
using Sk by (auto simp add: subset_eq) 

580 
ultimately have "?L (\<Union>K)" by blast 

581 
} 

44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

582 
ultimately show ?thesis 
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

583 
unfolding subset_eq mem_Collect_eq istopology_def by blast 
33175  584 
qed 
585 

53255  586 
lemma openin_subtopology: "openin (subtopology U V) S \<longleftrightarrow> (\<exists>T. openin U T \<and> S = T \<inter> V)" 
33175  587 
unfolding subtopology_def topology_inverse'[OF istopology_subtopology] 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

588 
by auto 
33175  589 

53255  590 
lemma topspace_subtopology: "topspace (subtopology U V) = topspace U \<inter> V" 
33175  591 
by (auto simp add: topspace_def openin_subtopology) 
592 

53255  593 
lemma closedin_subtopology: "closedin (subtopology U V) S \<longleftrightarrow> (\<exists>T. closedin U T \<and> S = T \<inter> V)" 
33175  594 
unfolding closedin_def topspace_subtopology 
55775  595 
by (auto simp add: openin_subtopology) 
33175  596 

597 
lemma openin_subtopology_refl: "openin (subtopology U V) V \<longleftrightarrow> V \<subseteq> topspace U" 

598 
unfolding openin_subtopology 

55775  599 
by auto (metis IntD1 in_mono openin_subset) 
49711  600 

601 
lemma subtopology_superset: 

602 
assumes UV: "topspace U \<subseteq> V" 

33175  603 
shows "subtopology U V = U" 
53255  604 
proof  
605 
{ 

606 
fix S 

607 
{ 

608 
fix T 

609 
assume T: "openin U T" "S = T \<inter> V" 

610 
from T openin_subset[OF T(1)] UV have eq: "S = T" 

611 
by blast 

612 
have "openin U S" 

613 
unfolding eq using T by blast 

614 
} 

33175  615 
moreover 
53255  616 
{ 
617 
assume S: "openin U S" 

618 
then have "\<exists>T. openin U T \<and> S = T \<inter> V" 

619 
using openin_subset[OF S] UV by auto 

620 
} 

621 
ultimately have "(\<exists>T. openin U T \<and> S = T \<inter> V) \<longleftrightarrow> openin U S" 

622 
by blast 

623 
} 

624 
then show ?thesis 

625 
unfolding topology_eq openin_subtopology by blast 

33175  626 
qed 
627 

628 
lemma subtopology_topspace[simp]: "subtopology U (topspace U) = U" 

629 
by (simp add: subtopology_superset) 

630 

631 
lemma subtopology_UNIV[simp]: "subtopology U UNIV = U" 

632 
by (simp add: subtopology_superset) 

633 

53255  634 

44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

635 
subsubsection {* The standard Euclidean topology *} 
33175  636 

53255  637 
definition euclidean :: "'a::topological_space topology" 
638 
where "euclidean = topology open" 

33175  639 

640 
lemma open_openin: "open S \<longleftrightarrow> openin euclidean S" 

641 
unfolding euclidean_def 

642 
apply (rule cong[where x=S and y=S]) 

643 
apply (rule topology_inverse[symmetric]) 

644 
apply (auto simp add: istopology_def) 

44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

645 
done 
33175  646 

647 
lemma topspace_euclidean: "topspace euclidean = UNIV" 

648 
apply (simp add: topspace_def) 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

649 
apply (rule set_eqI) 
53255  650 
apply (auto simp add: open_openin[symmetric]) 
651 
done 

33175  652 

653 
lemma topspace_euclidean_subtopology[simp]: "topspace (subtopology euclidean S) = S" 

654 
by (simp add: topspace_euclidean topspace_subtopology) 

655 

656 
lemma closed_closedin: "closed S \<longleftrightarrow> closedin euclidean S" 

657 
by (simp add: closed_def closedin_def topspace_euclidean open_openin Compl_eq_Diff_UNIV) 

658 

659 
lemma open_subopen: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S)" 

660 
by (simp add: open_openin openin_subopen[symmetric]) 

661 

44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

662 
text {* Basic "localization" results are handy for connectedness. *} 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

663 

eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

664 
lemma openin_open: "openin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. open T \<and> (S = U \<inter> T))" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

665 
by (auto simp add: openin_subtopology open_openin[symmetric]) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

666 

eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

667 
lemma openin_open_Int[intro]: "open S \<Longrightarrow> openin (subtopology euclidean U) (U \<inter> S)" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

668 
by (auto simp add: openin_open) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

669 

eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

670 
lemma open_openin_trans[trans]: 
53255  671 
"open S \<Longrightarrow> open T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> openin (subtopology euclidean S) T" 
44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

672 
by (metis Int_absorb1 openin_open_Int) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

673 

53255  674 
lemma open_subset: "S \<subseteq> T \<Longrightarrow> open S \<Longrightarrow> openin (subtopology euclidean T) S" 
44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

675 
by (auto simp add: openin_open) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

676 

eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

677 
lemma closedin_closed: "closedin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. closed T \<and> S = U \<inter> T)" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

678 
by (simp add: closedin_subtopology closed_closedin Int_ac) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

679 

53291  680 
lemma closedin_closed_Int: "closed S \<Longrightarrow> closedin (subtopology euclidean U) (U \<inter> S)" 
44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

681 
by (metis closedin_closed) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

682 

53282  683 
lemma closed_closedin_trans: 
684 
"closed S \<Longrightarrow> closed T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> closedin (subtopology euclidean S) T" 

55775  685 
by (metis closedin_closed inf.absorb2) 
44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

686 

eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

687 
lemma closed_subset: "S \<subseteq> T \<Longrightarrow> closed S \<Longrightarrow> closedin (subtopology euclidean T) S" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

688 
by (auto simp add: closedin_closed) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

689 

eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

690 
lemma openin_euclidean_subtopology_iff: 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

691 
fixes S U :: "'a::metric_space set" 
53255  692 
shows "openin (subtopology euclidean U) S \<longleftrightarrow> 
693 
S \<subseteq> U \<and> (\<forall>x\<in>S. \<exists>e>0. \<forall>x'\<in>U. dist x' x < e \<longrightarrow> x'\<in> S)" 

694 
(is "?lhs \<longleftrightarrow> ?rhs") 

44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

695 
proof 
53255  696 
assume ?lhs 
53282  697 
then show ?rhs 
698 
unfolding openin_open open_dist by blast 

44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

699 
next 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

700 
def T \<equiv> "{x. \<exists>a\<in>S. \<exists>d>0. (\<forall>y\<in>U. dist y a < d \<longrightarrow> y \<in> S) \<and> dist x a < d}" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

701 
have 1: "\<forall>x\<in>T. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> T" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

702 
unfolding T_def 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

703 
apply clarsimp 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

704 
apply (rule_tac x="d  dist x a" in exI) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

705 
apply (clarsimp simp add: less_diff_eq) 
55775  706 
by (metis dist_commute dist_triangle_lt) 
53282  707 
assume ?rhs then have 2: "S = U \<inter> T" 
55775  708 
unfolding T_def 
709 
by auto (metis dist_self) 

44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

710 
from 1 2 show ?lhs 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

711 
unfolding openin_open open_dist by fast 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

712 
qed 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

713 

eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

714 
text {* These "transitivity" results are handy too *} 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

715 

53255  716 
lemma openin_trans[trans]: 
717 
"openin (subtopology euclidean T) S \<Longrightarrow> openin (subtopology euclidean U) T \<Longrightarrow> 

718 
openin (subtopology euclidean U) S" 

44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

719 
unfolding open_openin openin_open by blast 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

720 

eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

721 
lemma openin_open_trans: "openin (subtopology euclidean T) S \<Longrightarrow> open T \<Longrightarrow> open S" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

722 
by (auto simp add: openin_open intro: openin_trans) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

723 

eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

724 
lemma closedin_trans[trans]: 
53255  725 
"closedin (subtopology euclidean T) S \<Longrightarrow> closedin (subtopology euclidean U) T \<Longrightarrow> 
726 
closedin (subtopology euclidean U) S" 

44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

727 
by (auto simp add: closedin_closed closed_closedin closed_Inter Int_assoc) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

728 

eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

729 
lemma closedin_closed_trans: "closedin (subtopology euclidean T) S \<Longrightarrow> closed T \<Longrightarrow> closed S" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

730 
by (auto simp add: closedin_closed intro: closedin_trans) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

731 

eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

732 

eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

733 
subsection {* Open and closed balls *} 
33175  734 

53255  735 
definition ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" 
736 
where "ball x e = {y. dist x y < e}" 

737 

738 
definition cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" 

739 
where "cball x e = {y. dist x y \<le> e}" 

33175  740 

45776
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

741 
lemma mem_ball [simp]: "y \<in> ball x e \<longleftrightarrow> dist x y < e" 
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

742 
by (simp add: ball_def) 
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

743 

714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

744 
lemma mem_cball [simp]: "y \<in> cball x e \<longleftrightarrow> dist x y \<le> e" 
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

745 
by (simp add: cball_def) 
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

746 

714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

747 
lemma mem_ball_0: 
33175  748 
fixes x :: "'a::real_normed_vector" 
749 
shows "x \<in> ball 0 e \<longleftrightarrow> norm x < e" 

750 
by (simp add: dist_norm) 

751 

45776
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

752 
lemma mem_cball_0: 
33175  753 
fixes x :: "'a::real_normed_vector" 
754 
shows "x \<in> cball 0 e \<longleftrightarrow> norm x \<le> e" 

755 
by (simp add: dist_norm) 

756 

45776
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

757 
lemma centre_in_ball: "x \<in> ball x e \<longleftrightarrow> 0 < e" 
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

758 
by simp 
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

759 

714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

760 
lemma centre_in_cball: "x \<in> cball x e \<longleftrightarrow> 0 \<le> e" 
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

761 
by simp 
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

762 

53255  763 
lemma ball_subset_cball[simp,intro]: "ball x e \<subseteq> cball x e" 
764 
by (simp add: subset_eq) 

765 

53282  766 
lemma subset_ball[intro]: "d \<le> e \<Longrightarrow> ball x d \<subseteq> ball x e" 
53255  767 
by (simp add: subset_eq) 
768 

53282  769 
lemma subset_cball[intro]: "d \<le> e \<Longrightarrow> cball x d \<subseteq> cball x e" 
53255  770 
by (simp add: subset_eq) 
771 

33175  772 
lemma ball_max_Un: "ball a (max r s) = ball a r \<union> ball a s" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

773 
by (simp add: set_eq_iff) arith 
33175  774 

775 
lemma ball_min_Int: "ball a (min r s) = ball a r \<inter> ball a s" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

776 
by (simp add: set_eq_iff) 
33175  777 

53255  778 
lemma diff_less_iff: 
779 
"(a::real)  b > 0 \<longleftrightarrow> a > b" 

33175  780 
"(a::real)  b < 0 \<longleftrightarrow> a < b" 
53255  781 
"a  b < c \<longleftrightarrow> a < c + b" "a  b > c \<longleftrightarrow> a > c + b" 
782 
by arith+ 

783 

784 
lemma diff_le_iff: 

785 
"(a::real)  b \<ge> 0 \<longleftrightarrow> a \<ge> b" 

786 
"(a::real)  b \<le> 0 \<longleftrightarrow> a \<le> b" 

787 
"a  b \<le> c \<longleftrightarrow> a \<le> c + b" 

788 
"a  b \<ge> c \<longleftrightarrow> a \<ge> c + b" 

789 
by arith+ 

33175  790 

54070  791 
lemma open_ball [intro, simp]: "open (ball x e)" 
792 
proof  

793 
have "open (dist x ` {..<e})" 

794 
by (intro open_vimage open_lessThan continuous_on_intros) 

795 
also have "dist x ` {..<e} = ball x e" 

796 
by auto 

797 
finally show ?thesis . 

798 
qed 

33175  799 

800 
lemma open_contains_ball: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. ball x e \<subseteq> S)" 

801 
unfolding open_dist subset_eq mem_ball Ball_def dist_commute .. 

802 

33714
eb2574ac4173
Added new lemmas to Euclidean Space by Robert Himmelmann
hoelzl
parents:
33324
diff
changeset

803 
lemma openE[elim?]: 
53282  804 
assumes "open S" "x\<in>S" 
33714
eb2574ac4173
Added new lemmas to Euclidean Space by Robert Himmelmann
hoelzl
parents:
33324
diff
changeset

805 
obtains e where "e>0" "ball x e \<subseteq> S" 
eb2574ac4173
Added new lemmas to Euclidean Space by Robert Himmelmann
hoelzl
parents:
33324
diff
changeset

806 
using assms unfolding open_contains_ball by auto 
eb2574ac4173
Added new lemmas to Euclidean Space by Robert Himmelmann
hoelzl
parents:
33324
diff
changeset

807 

33175  808 
lemma open_contains_ball_eq: "open S \<Longrightarrow> \<forall>x. x\<in>S \<longleftrightarrow> (\<exists>e>0. ball x e \<subseteq> S)" 
809 
by (metis open_contains_ball subset_eq centre_in_ball) 

810 

811 
lemma ball_eq_empty[simp]: "ball x e = {} \<longleftrightarrow> e \<le> 0" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

812 
unfolding mem_ball set_eq_iff 
33175  813 
apply (simp add: not_less) 
52624  814 
apply (metis zero_le_dist order_trans dist_self) 
815 
done 

33175  816 

53291  817 
lemma ball_empty[intro]: "e \<le> 0 \<Longrightarrow> ball x e = {}" by simp 
33175  818 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

819 
lemma euclidean_dist_l2: 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

820 
fixes x y :: "'a :: euclidean_space" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

821 
shows "dist x y = setL2 (\<lambda>i. dist (x \<bullet> i) (y \<bullet> i)) Basis" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

822 
unfolding dist_norm norm_eq_sqrt_inner setL2_def 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

823 
by (subst euclidean_inner) (simp add: power2_eq_square inner_diff_left) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

824 

56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

825 

c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

826 
subsection {* Boxes *} 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

827 

54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset

828 
definition (in euclidean_space) eucl_less (infix "<e" 50) 
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset

829 
where "eucl_less a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i)" 
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset

830 

2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset

831 
definition box_eucl_less: "box a b = {x. a <e x \<and> x <e b}" 
56188  832 
definition "cbox a b = {x. \<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i}" 
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset

833 

2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset

834 
lemma box_def: "box a b = {x. \<forall>i\<in>Basis. a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i}" 
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset

835 
and in_box_eucl_less: "x \<in> box a b \<longleftrightarrow> a <e x \<and> x <e b" 
56188  836 
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)" 
837 
"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)" 

838 
by (auto simp: box_eucl_less eucl_less_def cbox_def) 

839 

840 
lemma mem_box_real[simp]: 

841 
"(x::real) \<in> box a b \<longleftrightarrow> a < x \<and> x < b" 

842 
"(x::real) \<in> cbox a b \<longleftrightarrow> a \<le> x \<and> x \<le> b" 

843 
by (auto simp: mem_box) 

844 

845 
lemma box_real[simp]: 

846 
fixes a b:: real 

847 
shows "box a b = {a <..< b}" "cbox a b = {a .. b}" 

848 
by auto 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

849 

50087  850 
lemma rational_boxes: 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

851 
fixes x :: "'a\<Colon>euclidean_space" 
53291  852 
assumes "e > 0" 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

853 
shows "\<exists>a b. (\<forall>i\<in>Basis. a \<bullet> i \<in> \<rat> \<and> b \<bullet> i \<in> \<rat> ) \<and> x \<in> box a b \<and> box a b \<subseteq> ball x e" 
50087  854 
proof  
855 
def e' \<equiv> "e / (2 * sqrt (real (DIM ('a))))" 

53291  856 
then have e: "e' > 0" 
53255  857 
using assms by (auto intro!: divide_pos_pos simp: DIM_positive) 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

858 
have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x \<bullet> i \<and> x \<bullet> i  y < e'" (is "\<forall>i. ?th i") 
50087  859 
proof 
53255  860 
fix i 
861 
from Rats_dense_in_real[of "x \<bullet> i  e'" "x \<bullet> i"] e 

862 
show "?th i" by auto 

50087  863 
qed 
55522  864 
from choice[OF this] obtain a where 
865 
a: "\<forall>xa. a xa \<in> \<rat> \<and> a xa < x \<bullet> xa \<and> x \<bullet> xa  a xa < e'" .. 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

866 
have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x \<bullet> i < y \<and> y  x \<bullet> i < e'" (is "\<forall>i. ?th i") 
50087  867 
proof 
53255  868 
fix i 
869 
from Rats_dense_in_real[of "x \<bullet> i" "x \<bullet> i + e'"] e 

870 
show "?th i" by auto 

50087  871 
qed 
55522  872 
from choice[OF this] obtain b where 
873 
b: "\<forall>xa. b xa \<in> \<rat> \<and> x \<bullet> xa < b xa \<and> b xa  x \<bullet> xa < e'" .. 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

874 
let ?a = "\<Sum>i\<in>Basis. a i *\<^sub>R i" and ?b = "\<Sum>i\<in>Basis. b i *\<^sub>R i" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

875 
show ?thesis 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

876 
proof (rule exI[of _ ?a], rule exI[of _ ?b], safe) 
53255  877 
fix y :: 'a 
878 
assume *: "y \<in> box ?a ?b" 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52625
diff
changeset

879 
have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)" 
50087  880 
unfolding setL2_def[symmetric] by (rule euclidean_dist_l2) 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

881 
also have "\<dots> < sqrt (\<Sum>(i::'a)\<in>Basis. e^2 / real (DIM('a)))" 
50087  882 
proof (rule real_sqrt_less_mono, rule setsum_strict_mono) 
53255  883 
fix i :: "'a" 
884 
assume i: "i \<in> Basis" 

885 
have "a i < y\<bullet>i \<and> y\<bullet>i < b i" 

886 
using * i by (auto simp: box_def) 

887 
moreover have "a i < x\<bullet>i" "x\<bullet>i  a i < e'" 

888 
using a by auto 

889 
moreover have "x\<bullet>i < b i" "b i  x\<bullet>i < e'" 

890 
using b by auto 

891 
ultimately have "\<bar>x\<bullet>i  y\<bullet>i\<bar> < 2 * e'" 

892 
by auto 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

893 
then have "dist (x \<bullet> i) (y \<bullet> i) < e/sqrt (real (DIM('a)))" 
50087  894 
unfolding e'_def by (auto simp: dist_real_def) 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52625
diff
changeset

895 
then have "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < (e/sqrt (real (DIM('a))))\<^sup>2" 
50087  896 
by (rule power_strict_mono) auto 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52625
diff
changeset

897 
then show "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < e\<^sup>2 / real DIM('a)" 
50087  898 
by (simp add: power_divide) 
899 
qed auto 

53255  900 
also have "\<dots> = e" 
901 
using `0 < e` by (simp add: real_eq_of_nat) 

902 
finally show "y \<in> ball x e" 

903 
by (auto simp: ball_def) 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

904 
qed (insert a b, auto simp: box_def) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

905 
qed 
51103  906 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

907 
lemma open_UNION_box: 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

908 
fixes M :: "'a\<Colon>euclidean_space set" 
53282  909 
assumes "open M" 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

910 
defines "a' \<equiv> \<lambda>f :: 'a \<Rightarrow> real \<times> real. (\<Sum>(i::'a)\<in>Basis. fst (f i) *\<^sub>R i)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

911 
defines "b' \<equiv> \<lambda>f :: 'a \<Rightarrow> real \<times> real. (\<Sum>(i::'a)\<in>Basis. snd (f i) *\<^sub>R i)" 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52625
diff
changeset

912 
defines "I \<equiv> {f\<in>Basis \<rightarrow>\<^sub>E \<rat> \<times> \<rat>. box (a' f) (b' f) \<subseteq> M}" 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

913 
shows "M = (\<Union>f\<in>I. box (a' f) (b' f))" 
52624  914 
proof  
915 
{ 

916 
fix x assume "x \<in> M" 

917 
obtain e where e: "e > 0" "ball x e \<subseteq> M" 

918 
using openE[OF `open M` `x \<in> M`] by auto 

53282  919 
moreover obtain a b where ab: 
920 
"x \<in> box a b" 

921 
"\<forall>i \<in> Basis. a \<bullet> i \<in> \<rat>" 

922 
"\<forall>i\<in>Basis. b \<bullet> i \<in> \<rat>" 

923 
"box a b \<subseteq> ball x e" 

52624  924 
using rational_boxes[OF e(1)] by metis 
925 
ultimately have "x \<in> (\<Union>f\<in>I. box (a' f) (b' f))" 

926 
by (intro UN_I[of "\<lambda>i\<in>Basis. (a \<bullet> i, b \<bullet> i)"]) 

927 
(auto simp: euclidean_representation I_def a'_def b'_def) 

928 
} 

929 
then show ?thesis by (auto simp: I_def) 

930 
qed 

931 

56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

932 
lemma box_eq_empty: 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

933 
fixes a :: "'a::euclidean_space" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

934 
shows "(box a b = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i))" (is ?th1) 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

935 
and "(cbox a b = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i < a\<bullet>i))" (is ?th2) 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

936 
proof  
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

937 
{ 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

938 
fix i x 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

939 
assume i: "i\<in>Basis" and as:"b\<bullet>i \<le> a\<bullet>i" and x:"x\<in>box a b" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

940 
then have "a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

941 
unfolding mem_box by (auto simp: box_def) 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

942 
then have "a\<bullet>i < b\<bullet>i" by auto 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

943 
then have False using as by auto 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

944 
} 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

945 
moreover 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

946 
{ 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

947 
assume as: "\<forall>i\<in>Basis. \<not> (b\<bullet>i \<le> a\<bullet>i)" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

948 
let ?x = "(1/2) *\<^sub>R (a + b)" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

949 
{ 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

950 
fix i :: 'a 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

951 
assume i: "i \<in> Basis" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

952 
have "a\<bullet>i < b\<bullet>i" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

953 
using as[THEN bspec[where x=i]] i by auto 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

954 
then have "a\<bullet>i < ((1/2) *\<^sub>R (a+b)) \<bullet> i" "((1/2) *\<^sub>R (a+b)) \<bullet> i < b\<bullet>i" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

955 
by (auto simp: inner_add_left) 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

956 
} 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

957 
then have "box a b \<noteq> {}" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

958 
using mem_box(1)[of "?x" a b] by auto 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

959 
} 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

960 
ultimately show ?th1 by blast 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

961 

c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

962 
{ 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

963 
fix i x 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

964 
assume i: "i \<in> Basis" and as:"b\<bullet>i < a\<bullet>i" and x:"x\<in>cbox a b" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

965 
then have "a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

966 
unfolding mem_box by auto 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

967 
then have "a\<bullet>i \<le> b\<bullet>i" by auto 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

968 
then have False using as by auto 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

969 
} 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

970 
moreover 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

971 
{ 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

972 
assume as:"\<forall>i\<in>Basis. \<not> (b\<bullet>i < a\<bullet>i)" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

973 
let ?x = "(1/2) *\<^sub>R (a + b)" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

974 
{ 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

975 
fix i :: 'a 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

976 
assume i:"i \<in> Basis" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

977 
have "a\<bullet>i \<le> b\<bullet>i" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

978 
using as[THEN bspec[where x=i]] i by auto 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

979 
then have "a\<bullet>i \<le> ((1/2) *\<^sub>R (a+b)) \<bullet> i" "((1/2) *\<^sub>R (a+b)) \<bullet> i \<le> b\<bullet>i" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

980 
by (auto simp: inner_add_left) 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

981 
} 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

982 
then have "cbox a b \<noteq> {}" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

983 
using mem_box(2)[of "?x" a b] by auto 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

984 
} 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

985 
ultimately show ?th2 by blast 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

986 
qed 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

987 

c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

988 
lemma box_ne_empty: 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

989 
fixes a :: "'a::euclidean_space" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

990 
shows "cbox a b \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i)" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

991 
and "box a b \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

992 
unfolding box_eq_empty[of a b] by fastforce+ 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

993 

c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

994 
lemma 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

995 
fixes a :: "'a::euclidean_space" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

996 
shows cbox_sing: "cbox a a = {a}" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

997 
and box_sing: "box a a = {}" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

998 
unfolding set_eq_iff mem_box eq_iff [symmetric] 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

999 
by (auto intro!: euclidean_eqI[where 'a='a]) 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1000 
(metis all_not_in_conv nonempty_Basis) 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1001 

c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1002 
lemma subset_box_imp: 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1003 
fixes a :: "'a::euclidean_space" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1004 
shows "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> cbox c d \<subseteq> cbox a b" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1005 
and "(\<forall>i\<in>Basis. a\<bullet>i < c\<bullet>i \<and> d\<bullet>i < b\<bullet>i) \<Longrightarrow> cbox c d \<subseteq> box a b" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1006 
and "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> box c d \<subseteq> cbox a b" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1007 
and "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> box c d \<subseteq> box a b" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1008 
unfolding subset_eq[unfolded Ball_def] unfolding mem_box 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1009 
by (best intro: order_trans less_le_trans le_less_trans less_imp_le)+ 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1010 

c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1011 
lemma box_subset_cbox: 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1012 
fixes a :: "'a::euclidean_space" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1013 
shows "box a b \<subseteq> cbox a b" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1014 
unfolding subset_eq [unfolded Ball_def] mem_box 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1015 
by (fast intro: less_imp_le) 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1016 

c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1017 
lemma subset_box: 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1018 
fixes a :: "'a::euclidean_space" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1019 
shows "cbox c d \<subseteq> cbox a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i \<le> d\<bullet>i) > (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th1) 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1020 
and "cbox c d \<subseteq> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i \<le> d\<bullet>i) > (\<forall>i\<in>Basis. a\<bullet>i < c\<bullet>i \<and> d\<bullet>i < b\<bullet>i)" (is ?th2) 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1021 
and "box c d \<subseteq> cbox a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) > (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th3) 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1022 
and "box c d \<subseteq> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) > (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th4) 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1023 
proof  
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1024 
show ?th1 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1025 
unfolding subset_eq and Ball_def and mem_box 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1026 
by (auto intro: order_trans) 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1027 
show ?th2 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1028 
unfolding subset_eq and Ball_def and mem_box 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1029 
by (auto intro: le_less_trans less_le_trans order_trans less_imp_le) 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1030 
{ 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1031 
assume as: "box c d \<subseteq> cbox a b" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1032 
then have "box c d \<noteq> {}" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1033 
unfolding box_eq_empty by auto 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1034 
fix i :: 'a 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1035 
assume i: "i \<in> Basis" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1036 
(** TODO combine the following two parts as done in the HOL_light version. **) 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1037 
{ 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1038 
let ?x = "(\<Sum>j\<in>Basis. (if j=i then ((min (a\<bullet>j) (d\<bullet>j))+c\<bullet>j)/2 else (c\<bullet>j+d\<bullet>j)/2) *\<^sub>R j)::'a" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1039 
assume as2: "a\<bullet>i > c\<bullet>i" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1040 
{ 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1041 
fix j :: 'a 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1042 
assume j: "j \<in> Basis" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1043 
then have "c \<bullet> j < ?x \<bullet> j \<and> ?x \<bullet> j < d \<bullet> j" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1044 
apply (cases "j = i") 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1045 
using as(2)[THEN bspec[where x=j]] i 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1046 
apply (auto simp add: as2) 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1047 
done 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1048 
} 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1049 
then have "?x\<in>box c d" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1050 
using i unfolding mem_box by auto 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1051 
moreover 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1052 
have "?x \<notin> cbox a b" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1053 
unfolding mem_box 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1054 
apply auto 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1055 
apply (rule_tac x=i in bexI) 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1056 
using as(2)[THEN bspec[where x=i]] and as2 i 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1057 
apply auto 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1058 
done 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1059 
ultimately have False using as by auto 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1060 
} 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1061 
then have "a\<bullet>i \<le> c\<bullet>i" by (rule ccontr) auto 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1062 
moreover 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1063 
{ 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1064 
let ?x = "(\<Sum>j\<in>Basis. (if j=i then ((max (b\<bullet>j) (c\<bullet>j))+d\<bullet>j)/2 else (c\<bullet>j+d\<bullet>j)/2) *\<^sub>R j)::'a" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1065 
assume as2: "b\<bullet>i < d\<bullet>i" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1066 
{ 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1067 
fix j :: 'a 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1068 
assume "j\<in>Basis" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1069 
then have "d \<bullet> j > ?x \<bullet> j \<and> ?x \<bullet> j > c \<bullet> j" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1070 
apply (cases "j = i") 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1071 
using as(2)[THEN bspec[where x=j]] 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1072 
apply (auto simp add: as2) 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1073 
done 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1074 
} 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1075 
then have "?x\<in>box c d" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1076 
unfolding mem_box by auto 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1077 
moreover 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1078 
have "?x\<notin>cbox a b" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1079 
unfolding mem_box 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1080 
apply auto 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1081 
apply (rule_tac x=i in bexI) 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1082 
using as(2)[THEN bspec[where x=i]] and as2 using i 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1083 
apply auto 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1084 
done 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1085 
ultimately have False using as by auto 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1086 
} 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1087 
then have "b\<bullet>i \<ge> d\<bullet>i" by (rule ccontr) auto 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1088 
ultimately 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1089 
have "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i" by auto 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1090 
} note part1 = this 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1091 
show ?th3 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1092 
unfolding subset_eq and Ball_def and mem_box 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1093 
apply (rule, rule, rule, rule) 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1094 
apply (rule part1) 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1095 
unfolding subset_eq and Ball_def and mem_box 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1096 
prefer 4 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1097 
apply auto 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1098 
apply (erule_tac x=xa in allE, erule_tac x=xa in allE, fastforce)+ 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1099 
done 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1100 
{ 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1101 
assume as: "box c d \<subseteq> box a b" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1102 
fix i :: 'a 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1103 
assume i:"i\<in>Basis" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1104 
from as(1) have "box c d \<subseteq> cbox a b" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1105 
using box_subset_cbox[of a b] by auto 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1106 
then have "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1107 
using part1 and as(2) using i by auto 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1108 
} note * = this 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1109 
show ?th4 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1110 
unfolding subset_eq and Ball_def and mem_box 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1111 
apply (rule, rule, rule, rule) 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1112 
apply (rule *) 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1113 
unfolding subset_eq and Ball_def and mem_box 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1114 
prefer 4 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1115 
apply auto 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1116 
apply (erule_tac x=xa in allE, simp)+ 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1117 
done 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1118 
qed 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1119 

c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1120 
lemma inter_interval: 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1121 
fixes a :: "'a::euclidean_space" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1122 
shows "cbox a b \<inter> cbox c d = 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1123 
cbox (\<Sum>i\<in>Basis. max (a\<bullet>i) (c\<bullet>i) *\<^sub>R i) (\<Sum>i\<in>Basis. min (b\<bullet>i) (d\<bullet>i) *\<^sub>R i)" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1124 
unfolding set_eq_iff and Int_iff and mem_box 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1125 
by auto 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1126 

c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1127 
lemma disjoint_interval: 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1128 
fixes a::"'a::euclidean_space" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1129 
shows "cbox a b \<inter> cbox c d = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i < a\<bullet>i \<or> d\<bullet>i < c\<bullet>i \<or> b\<bullet>i < c\<bullet>i \<or> d\<bullet>i < a\<bullet>i))" (is ?th1) 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1130 
and "cbox a b \<inter> box c d = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i < a\<bullet>i \<or> d\<bullet>i \<le> c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th2) 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1131 
and "box a b \<inter> cbox c d = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i \<le> a\<bullet>i \<or> d\<bullet>i < c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th3) 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1132 
and "box a b \<inter> box c d = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i \<le> a\<bullet>i \<or> d\<bullet>i \<le> c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th4) 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1133 
proof  
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1134 
let ?z = "(\<Sum>i\<in>Basis. (((max (a\<bullet>i) (c\<bullet>i)) + (min (b\<bullet>i) (d\<bullet>i))) / 2) *\<^sub>R i)::'a" 
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
< 