hoelzl@33714
|
1 |
(* title: HOL/Library/Topology_Euclidian_Space.thy
|
himmelma@33175
|
2 |
Author: Amine Chaieb, University of Cambridge
|
himmelma@33175
|
3 |
Author: Robert Himmelmann, TU Muenchen
|
huffman@44075
|
4 |
Author: Brian Huffman, Portland State University
|
himmelma@33175
|
5 |
*)
|
himmelma@33175
|
6 |
|
wenzelm@60420
|
7 |
section \<open>Elementary topology in Euclidean space.\<close>
|
himmelma@33175
|
8 |
|
himmelma@33175
|
9 |
theory Topology_Euclidean_Space
|
immler@50087
|
10 |
imports
|
hoelzl@50938
|
11 |
Complex_Main
|
immler@50245
|
12 |
"~~/src/HOL/Library/Countable_Set"
|
hoelzl@50526
|
13 |
"~~/src/HOL/Library/FuncSet"
|
hoelzl@50938
|
14 |
Linear_Algebra
|
immler@50087
|
15 |
Norm_Arith
|
immler@50087
|
16 |
begin
|
immler@50087
|
17 |
|
hoelzl@50972
|
18 |
lemma dist_0_norm:
|
hoelzl@50972
|
19 |
fixes x :: "'a::real_normed_vector"
|
hoelzl@50972
|
20 |
shows "dist 0 x = norm x"
|
hoelzl@50972
|
21 |
unfolding dist_norm by simp
|
hoelzl@50972
|
22 |
|
hoelzl@50943
|
23 |
lemma dist_double: "dist x y < d / 2 \<Longrightarrow> dist x z < d / 2 \<Longrightarrow> dist y z < d"
|
hoelzl@50943
|
24 |
using dist_triangle[of y z x] by (simp add: dist_commute)
|
hoelzl@50943
|
25 |
|
hoelzl@50972
|
26 |
(* LEGACY *)
|
wenzelm@53640
|
27 |
lemma lim_subseq: "subseq r \<Longrightarrow> s ----> l \<Longrightarrow> (s \<circ> r) ----> l"
|
hoelzl@50972
|
28 |
by (rule LIMSEQ_subseq_LIMSEQ)
|
hoelzl@50972
|
29 |
|
wenzelm@53282
|
30 |
lemma countable_PiE:
|
hoelzl@50526
|
31 |
"finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (PiE I F)"
|
hoelzl@50526
|
32 |
by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq)
|
hoelzl@50526
|
33 |
|
hoelzl@51481
|
34 |
lemma Lim_within_open:
|
hoelzl@51481
|
35 |
fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
|
hoelzl@51481
|
36 |
shows "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f ---> l)(at a within S) \<longleftrightarrow> (f ---> l)(at a)"
|
hoelzl@51481
|
37 |
by (fact tendsto_within_open)
|
hoelzl@51481
|
38 |
|
hoelzl@51481
|
39 |
lemma continuous_on_union:
|
hoelzl@51481
|
40 |
"closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f"
|
hoelzl@51481
|
41 |
by (fact continuous_on_closed_Un)
|
hoelzl@51481
|
42 |
|
hoelzl@51481
|
43 |
lemma continuous_on_cases:
|
hoelzl@51481
|
44 |
"closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t g \<Longrightarrow>
|
hoelzl@51481
|
45 |
\<forall>x. (x\<in>s \<and> \<not> P x) \<or> (x \<in> t \<and> P x) \<longrightarrow> f x = g x \<Longrightarrow>
|
hoelzl@51481
|
46 |
continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)"
|
hoelzl@51481
|
47 |
by (rule continuous_on_If) auto
|
hoelzl@51481
|
48 |
|
wenzelm@53255
|
49 |
|
wenzelm@60420
|
50 |
subsection \<open>Topological Basis\<close>
|
immler@50087
|
51 |
|
immler@50087
|
52 |
context topological_space
|
immler@50087
|
53 |
begin
|
immler@50087
|
54 |
|
wenzelm@53291
|
55 |
definition "topological_basis B \<longleftrightarrow>
|
wenzelm@53291
|
56 |
(\<forall>b\<in>B. open b) \<and> (\<forall>x. open x \<longrightarrow> (\<exists>B'. B' \<subseteq> B \<and> \<Union>B' = x))"
|
hoelzl@51343
|
57 |
|
hoelzl@51343
|
58 |
lemma topological_basis:
|
wenzelm@53291
|
59 |
"topological_basis B \<longleftrightarrow> (\<forall>x. open x \<longleftrightarrow> (\<exists>B'. B' \<subseteq> B \<and> \<Union>B' = x))"
|
hoelzl@50998
|
60 |
unfolding topological_basis_def
|
hoelzl@50998
|
61 |
apply safe
|
hoelzl@50998
|
62 |
apply fastforce
|
hoelzl@50998
|
63 |
apply fastforce
|
hoelzl@50998
|
64 |
apply (erule_tac x="x" in allE)
|
hoelzl@50998
|
65 |
apply simp
|
hoelzl@50998
|
66 |
apply (rule_tac x="{x}" in exI)
|
hoelzl@50998
|
67 |
apply auto
|
hoelzl@50998
|
68 |
done
|
hoelzl@50998
|
69 |
|
immler@50087
|
70 |
lemma topological_basis_iff:
|
immler@50087
|
71 |
assumes "\<And>B'. B' \<in> B \<Longrightarrow> open B'"
|
immler@50087
|
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'))"
|
immler@50087
|
73 |
(is "_ \<longleftrightarrow> ?rhs")
|
immler@50087
|
74 |
proof safe
|
immler@50087
|
75 |
fix O' and x::'a
|
immler@50087
|
76 |
assume H: "topological_basis B" "open O'" "x \<in> O'"
|
wenzelm@53282
|
77 |
then have "(\<exists>B'\<subseteq>B. \<Union>B' = O')" by (simp add: topological_basis_def)
|
immler@50087
|
78 |
then obtain B' where "B' \<subseteq> B" "O' = \<Union>B'" by auto
|
wenzelm@53282
|
79 |
then show "\<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'" using H by auto
|
immler@50087
|
80 |
next
|
immler@50087
|
81 |
assume H: ?rhs
|
wenzelm@53282
|
82 |
show "topological_basis B"
|
wenzelm@53282
|
83 |
using assms unfolding topological_basis_def
|
immler@50087
|
84 |
proof safe
|
wenzelm@53640
|
85 |
fix O' :: "'a set"
|
wenzelm@53282
|
86 |
assume "open O'"
|
immler@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'"
|
immler@50087
|
88 |
by (force intro: bchoice simp: Bex_def)
|
wenzelm@53282
|
89 |
then show "\<exists>B'\<subseteq>B. \<Union>B' = O'"
|
immler@50087
|
90 |
by (auto intro: exI[where x="{f x |x. x \<in> O'}"])
|
immler@50087
|
91 |
qed
|
immler@50087
|
92 |
qed
|
immler@50087
|
93 |
|
immler@50087
|
94 |
lemma topological_basisI:
|
immler@50087
|
95 |
assumes "\<And>B'. B' \<in> B \<Longrightarrow> open B'"
|
wenzelm@53282
|
96 |
and "\<And>O' x. open O' \<Longrightarrow> x \<in> O' \<Longrightarrow> \<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'"
|
immler@50087
|
97 |
shows "topological_basis B"
|
immler@50087
|
98 |
using assms by (subst topological_basis_iff) auto
|
immler@50087
|
99 |
|
immler@50087
|
100 |
lemma topological_basisE:
|
immler@50087
|
101 |
fixes O'
|
immler@50087
|
102 |
assumes "topological_basis B"
|
wenzelm@53282
|
103 |
and "open O'"
|
wenzelm@53282
|
104 |
and "x \<in> O'"
|
immler@50087
|
105 |
obtains B' where "B' \<in> B" "x \<in> B'" "B' \<subseteq> O'"
|
immler@50087
|
106 |
proof atomize_elim
|
wenzelm@53282
|
107 |
from assms have "\<And>B'. B'\<in>B \<Longrightarrow> open B'"
|
wenzelm@53282
|
108 |
by (simp add: topological_basis_def)
|
immler@50087
|
109 |
with topological_basis_iff assms
|
wenzelm@53282
|
110 |
show "\<exists>B'. B' \<in> B \<and> x \<in> B' \<and> B' \<subseteq> O'"
|
wenzelm@53282
|
111 |
using assms by (simp add: Bex_def)
|
immler@50087
|
112 |
qed
|
immler@50087
|
113 |
|
immler@50094
|
114 |
lemma topological_basis_open:
|
immler@50094
|
115 |
assumes "topological_basis B"
|
wenzelm@53282
|
116 |
and "X \<in> B"
|
immler@50094
|
117 |
shows "open X"
|
wenzelm@53282
|
118 |
using assms by (simp add: topological_basis_def)
|
immler@50094
|
119 |
|
hoelzl@51343
|
120 |
lemma topological_basis_imp_subbasis:
|
wenzelm@53255
|
121 |
assumes B: "topological_basis B"
|
wenzelm@53255
|
122 |
shows "open = generate_topology B"
|
hoelzl@51343
|
123 |
proof (intro ext iffI)
|
wenzelm@53255
|
124 |
fix S :: "'a set"
|
wenzelm@53255
|
125 |
assume "open S"
|
hoelzl@51343
|
126 |
with B obtain B' where "B' \<subseteq> B" "S = \<Union>B'"
|
hoelzl@51343
|
127 |
unfolding topological_basis_def by blast
|
hoelzl@51343
|
128 |
then show "generate_topology B S"
|
hoelzl@51343
|
129 |
by (auto intro: generate_topology.intros dest: topological_basis_open)
|
hoelzl@51343
|
130 |
next
|
wenzelm@53255
|
131 |
fix S :: "'a set"
|
wenzelm@53255
|
132 |
assume "generate_topology B S"
|
wenzelm@53255
|
133 |
then show "open S"
|
hoelzl@51343
|
134 |
by induct (auto dest: topological_basis_open[OF B])
|
hoelzl@51343
|
135 |
qed
|
hoelzl@51343
|
136 |
|
immler@50245
|
137 |
lemma basis_dense:
|
wenzelm@53640
|
138 |
fixes B :: "'a set set"
|
wenzelm@53640
|
139 |
and f :: "'a set \<Rightarrow> 'a"
|
immler@50245
|
140 |
assumes "topological_basis B"
|
wenzelm@53255
|
141 |
and choosefrom_basis: "\<And>B'. B' \<noteq> {} \<Longrightarrow> f B' \<in> B'"
|
wenzelm@55522
|
142 |
shows "\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>B' \<in> B. f B' \<in> X)"
|
immler@50245
|
143 |
proof (intro allI impI)
|
wenzelm@53640
|
144 |
fix X :: "'a set"
|
wenzelm@53640
|
145 |
assume "open X" and "X \<noteq> {}"
|
wenzelm@60420
|
146 |
from topological_basisE[OF \<open>topological_basis B\<close> \<open>open X\<close> choosefrom_basis[OF \<open>X \<noteq> {}\<close>]]
|
wenzelm@55522
|
147 |
obtain B' where "B' \<in> B" "f X \<in> B'" "B' \<subseteq> X" .
|
wenzelm@53255
|
148 |
then show "\<exists>B'\<in>B. f B' \<in> X"
|
wenzelm@53255
|
149 |
by (auto intro!: choosefrom_basis)
|
immler@50245
|
150 |
qed
|
immler@50245
|
151 |
|
immler@50087
|
152 |
end
|
immler@50087
|
153 |
|
hoelzl@50882
|
154 |
lemma topological_basis_prod:
|
wenzelm@53255
|
155 |
assumes A: "topological_basis A"
|
wenzelm@53255
|
156 |
and B: "topological_basis B"
|
hoelzl@50882
|
157 |
shows "topological_basis ((\<lambda>(a, b). a \<times> b) ` (A \<times> B))"
|
hoelzl@50882
|
158 |
unfolding topological_basis_def
|
hoelzl@50882
|
159 |
proof (safe, simp_all del: ex_simps add: subset_image_iff ex_simps(1)[symmetric])
|
wenzelm@53255
|
160 |
fix S :: "('a \<times> 'b) set"
|
wenzelm@53255
|
161 |
assume "open S"
|
hoelzl@50882
|
162 |
then show "\<exists>X\<subseteq>A \<times> B. (\<Union>(a,b)\<in>X. a \<times> b) = S"
|
hoelzl@50882
|
163 |
proof (safe intro!: exI[of _ "{x\<in>A \<times> B. fst x \<times> snd x \<subseteq> S}"])
|
wenzelm@53255
|
164 |
fix x y
|
wenzelm@53255
|
165 |
assume "(x, y) \<in> S"
|
wenzelm@60420
|
166 |
from open_prod_elim[OF \<open>open S\<close> this]
|
hoelzl@50882
|
167 |
obtain a b where a: "open a""x \<in> a" and b: "open b" "y \<in> b" and "a \<times> b \<subseteq> S"
|
hoelzl@50882
|
168 |
by (metis mem_Sigma_iff)
|
wenzelm@55522
|
169 |
moreover
|
wenzelm@55522
|
170 |
from A a obtain A0 where "A0 \<in> A" "x \<in> A0" "A0 \<subseteq> a"
|
wenzelm@55522
|
171 |
by (rule topological_basisE)
|
wenzelm@55522
|
172 |
moreover
|
wenzelm@55522
|
173 |
from B b obtain B0 where "B0 \<in> B" "y \<in> B0" "B0 \<subseteq> b"
|
wenzelm@55522
|
174 |
by (rule topological_basisE)
|
hoelzl@50882
|
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)"
|
hoelzl@50882
|
176 |
by (intro UN_I[of "(A0, B0)"]) auto
|
hoelzl@50882
|
177 |
qed auto
|
hoelzl@50882
|
178 |
qed (metis A B topological_basis_open open_Times)
|
hoelzl@50882
|
179 |
|
wenzelm@53255
|
180 |
|
wenzelm@60420
|
181 |
subsection \<open>Countable Basis\<close>
|
immler@50245
|
182 |
|
immler@50245
|
183 |
locale countable_basis =
|
wenzelm@53640
|
184 |
fixes B :: "'a::topological_space set set"
|
immler@50245
|
185 |
assumes is_basis: "topological_basis B"
|
wenzelm@53282
|
186 |
and countable_basis: "countable B"
|
himmelma@33175
|
187 |
begin
|
himmelma@33175
|
188 |
|
immler@50245
|
189 |
lemma open_countable_basis_ex:
|
immler@50087
|
190 |
assumes "open X"
|
immler@50245
|
191 |
shows "\<exists>B' \<subseteq> B. X = Union B'"
|
wenzelm@53255
|
192 |
using assms countable_basis is_basis
|
wenzelm@53255
|
193 |
unfolding topological_basis_def by blast
|
immler@50245
|
194 |
|
immler@50245
|
195 |
lemma open_countable_basisE:
|
immler@50245
|
196 |
assumes "open X"
|
immler@50245
|
197 |
obtains B' where "B' \<subseteq> B" "X = Union B'"
|
wenzelm@53255
|
198 |
using assms open_countable_basis_ex
|
wenzelm@53255
|
199 |
by (atomize_elim) simp
|
immler@50245
|
200 |
|
immler@50245
|
201 |
lemma countable_dense_exists:
|
wenzelm@53291
|
202 |
"\<exists>D::'a set. countable D \<and> (\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>d \<in> D. d \<in> X))"
|
immler@50087
|
203 |
proof -
|
immler@50245
|
204 |
let ?f = "(\<lambda>B'. SOME x. x \<in> B')"
|
immler@50245
|
205 |
have "countable (?f ` B)" using countable_basis by simp
|
immler@50245
|
206 |
with basis_dense[OF is_basis, of ?f] show ?thesis
|
immler@50245
|
207 |
by (intro exI[where x="?f ` B"]) (metis (mono_tags) all_not_in_conv imageI someI)
|
immler@50087
|
208 |
qed
|
immler@50087
|
209 |
|
immler@50087
|
210 |
lemma countable_dense_setE:
|
immler@50245
|
211 |
obtains D :: "'a set"
|
immler@50245
|
212 |
where "countable D" "\<And>X. open X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> \<exists>d \<in> D. d \<in> X"
|
immler@50245
|
213 |
using countable_dense_exists by blast
|
immler@50245
|
214 |
|
immler@50087
|
215 |
end
|
immler@50087
|
216 |
|
hoelzl@50883
|
217 |
lemma (in first_countable_topology) first_countable_basisE:
|
hoelzl@50883
|
218 |
obtains A where "countable A" "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a"
|
hoelzl@50883
|
219 |
"\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)"
|
hoelzl@50883
|
220 |
using first_countable_basis[of x]
|
hoelzl@51473
|
221 |
apply atomize_elim
|
hoelzl@51473
|
222 |
apply (elim exE)
|
hoelzl@51473
|
223 |
apply (rule_tac x="range A" in exI)
|
hoelzl@51473
|
224 |
apply auto
|
hoelzl@51473
|
225 |
done
|
hoelzl@50883
|
226 |
|
immler@51105
|
227 |
lemma (in first_countable_topology) first_countable_basis_Int_stableE:
|
immler@51105
|
228 |
obtains A where "countable A" "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a"
|
immler@51105
|
229 |
"\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)"
|
immler@51105
|
230 |
"\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<inter> b \<in> A"
|
immler@51105
|
231 |
proof atomize_elim
|
wenzelm@55522
|
232 |
obtain A' where A':
|
wenzelm@55522
|
233 |
"countable A'"
|
wenzelm@55522
|
234 |
"\<And>a. a \<in> A' \<Longrightarrow> x \<in> a"
|
wenzelm@55522
|
235 |
"\<And>a. a \<in> A' \<Longrightarrow> open a"
|
wenzelm@55522
|
236 |
"\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>a\<in>A'. a \<subseteq> S"
|
wenzelm@55522
|
237 |
by (rule first_countable_basisE) blast
|
immler@51105
|
238 |
def A \<equiv> "(\<lambda>N. \<Inter>((\<lambda>n. from_nat_into A' n) ` N)) ` (Collect finite::nat set set)"
|
wenzelm@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>
|
immler@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)"
|
immler@51105
|
241 |
proof (safe intro!: exI[where x=A])
|
wenzelm@53255
|
242 |
show "countable A"
|
wenzelm@53255
|
243 |
unfolding A_def by (intro countable_image countable_Collect_finite)
|
wenzelm@53255
|
244 |
fix a
|
wenzelm@53255
|
245 |
assume "a \<in> A"
|
wenzelm@53255
|
246 |
then show "x \<in> a" "open a"
|
wenzelm@53255
|
247 |
using A'(4)[OF open_UNIV] by (auto simp: A_def intro: A' from_nat_into)
|
immler@51105
|
248 |
next
|
haftmann@52141
|
249 |
let ?int = "\<lambda>N. \<Inter>(from_nat_into A' ` N)"
|
wenzelm@53255
|
250 |
fix a b
|
wenzelm@53255
|
251 |
assume "a \<in> A" "b \<in> A"
|
wenzelm@53255
|
252 |
then obtain N M where "a = ?int N" "b = ?int M" "finite (N \<union> M)"
|
wenzelm@53255
|
253 |
by (auto simp: A_def)
|
wenzelm@53255
|
254 |
then show "a \<inter> b \<in> A"
|
wenzelm@53255
|
255 |
by (auto simp: A_def intro!: image_eqI[where x="N \<union> M"])
|
immler@51105
|
256 |
next
|
wenzelm@53255
|
257 |
fix S
|
wenzelm@53255
|
258 |
assume "open S" "x \<in> S"
|
wenzelm@53255
|
259 |
then obtain a where a: "a\<in>A'" "a \<subseteq> S" using A' by blast
|
wenzelm@53255
|
260 |
then show "\<exists>a\<in>A. a \<subseteq> S" using a A'
|
immler@51105
|
261 |
by (intro bexI[where x=a]) (auto simp: A_def intro: image_eqI[where x="{to_nat_on A' a}"])
|
immler@51105
|
262 |
qed
|
immler@51105
|
263 |
qed
|
immler@51105
|
264 |
|
hoelzl@51473
|
265 |
lemma (in topological_space) first_countableI:
|
wenzelm@53255
|
266 |
assumes "countable A"
|
wenzelm@53255
|
267 |
and 1: "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a"
|
wenzelm@53255
|
268 |
and 2: "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>a\<in>A. a \<subseteq> S"
|
hoelzl@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))"
|
hoelzl@51473
|
270 |
proof (safe intro!: exI[of _ "from_nat_into A"])
|
wenzelm@53255
|
271 |
fix i
|
hoelzl@51473
|
272 |
have "A \<noteq> {}" using 2[of UNIV] by auto
|
wenzelm@53255
|
273 |
show "x \<in> from_nat_into A i" "open (from_nat_into A i)"
|
wenzelm@60420
|
274 |
using range_from_nat_into_subset[OF \<open>A \<noteq> {}\<close>] 1 by auto
|
wenzelm@53255
|
275 |
next
|
wenzelm@53255
|
276 |
fix S
|
wenzelm@53255
|
277 |
assume "open S" "x\<in>S" from 2[OF this]
|
wenzelm@53255
|
278 |
show "\<exists>i. from_nat_into A i \<subseteq> S"
|
wenzelm@60420
|
279 |
using subset_range_from_nat_into[OF \<open>countable A\<close>] by auto
|
hoelzl@51473
|
280 |
qed
|
hoelzl@51350
|
281 |
|
hoelzl@50883
|
282 |
instance prod :: (first_countable_topology, first_countable_topology) first_countable_topology
|
hoelzl@50883
|
283 |
proof
|
hoelzl@50883
|
284 |
fix x :: "'a \<times> 'b"
|
wenzelm@55522
|
285 |
obtain A where A:
|
wenzelm@55522
|
286 |
"countable A"
|
wenzelm@55522
|
287 |
"\<And>a. a \<in> A \<Longrightarrow> fst x \<in> a"
|
wenzelm@55522
|
288 |
"\<And>a. a \<in> A \<Longrightarrow> open a"
|
wenzelm@55522
|
289 |
"\<And>S. open S \<Longrightarrow> fst x \<in> S \<Longrightarrow> \<exists>a\<in>A. a \<subseteq> S"
|
wenzelm@55522
|
290 |
by (rule first_countable_basisE[of "fst x"]) blast
|
wenzelm@55522
|
291 |
obtain B where B:
|
wenzelm@55522
|
292 |
"countable B"
|
wenzelm@55522
|
293 |
"\<And>a. a \<in> B \<Longrightarrow> snd x \<in> a"
|
wenzelm@55522
|
294 |
"\<And>a. a \<in> B \<Longrightarrow> open a"
|
wenzelm@55522
|
295 |
"\<And>S. open S \<Longrightarrow> snd x \<in> S \<Longrightarrow> \<exists>a\<in>B. a \<subseteq> S"
|
wenzelm@55522
|
296 |
by (rule first_countable_basisE[of "snd x"]) blast
|
wenzelm@53282
|
297 |
show "\<exists>A::nat \<Rightarrow> ('a \<times> 'b) set.
|
wenzelm@53282
|
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))"
|
hoelzl@51473
|
299 |
proof (rule first_countableI[of "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"], safe)
|
wenzelm@53255
|
300 |
fix a b
|
wenzelm@53255
|
301 |
assume x: "a \<in> A" "b \<in> B"
|
wenzelm@53640
|
302 |
with A(2, 3)[of a] B(2, 3)[of b] show "x \<in> a \<times> b" and "open (a \<times> b)"
|
wenzelm@53640
|
303 |
unfolding mem_Times_iff
|
wenzelm@53640
|
304 |
by (auto intro: open_Times)
|
hoelzl@50883
|
305 |
next
|
wenzelm@53255
|
306 |
fix S
|
wenzelm@53255
|
307 |
assume "open S" "x \<in> S"
|
wenzelm@55522
|
308 |
then obtain a' b' where a'b': "open a'" "open b'" "x \<in> a' \<times> b'" "a' \<times> b' \<subseteq> S"
|
wenzelm@55522
|
309 |
by (rule open_prod_elim)
|
wenzelm@55522
|
310 |
moreover
|
wenzelm@55522
|
311 |
from a'b' A(4)[of a'] B(4)[of b']
|
wenzelm@55522
|
312 |
obtain a b where "a \<in> A" "a \<subseteq> a'" "b \<in> B" "b \<subseteq> b'"
|
wenzelm@55522
|
313 |
by auto
|
wenzelm@55522
|
314 |
ultimately
|
wenzelm@55522
|
315 |
show "\<exists>a\<in>(\<lambda>(a, b). a \<times> b) ` (A \<times> B). a \<subseteq> S"
|
hoelzl@50883
|
316 |
by (auto intro!: bexI[of _ "a \<times> b"] bexI[of _ a] bexI[of _ b])
|
hoelzl@50883
|
317 |
qed (simp add: A B)
|
hoelzl@50883
|
318 |
qed
|
hoelzl@50883
|
319 |
|
hoelzl@50881
|
320 |
class second_countable_topology = topological_space +
|
wenzelm@53282
|
321 |
assumes ex_countable_subbasis:
|
wenzelm@53282
|
322 |
"\<exists>B::'a::topological_space set set. countable B \<and> open = generate_topology B"
|
hoelzl@51343
|
323 |
begin
|
hoelzl@51343
|
324 |
|
hoelzl@51343
|
325 |
lemma ex_countable_basis: "\<exists>B::'a set set. countable B \<and> topological_basis B"
|
hoelzl@51343
|
326 |
proof -
|
wenzelm@53255
|
327 |
from ex_countable_subbasis obtain B where B: "countable B" "open = generate_topology B"
|
wenzelm@53255
|
328 |
by blast
|
hoelzl@51343
|
329 |
let ?B = "Inter ` {b. finite b \<and> b \<subseteq> B }"
|
hoelzl@51343
|
330 |
|
hoelzl@51343
|
331 |
show ?thesis
|
hoelzl@51343
|
332 |
proof (intro exI conjI)
|
hoelzl@51343
|
333 |
show "countable ?B"
|
hoelzl@51343
|
334 |
by (intro countable_image countable_Collect_finite_subset B)
|
wenzelm@53255
|
335 |
{
|
wenzelm@53255
|
336 |
fix S
|
wenzelm@53255
|
337 |
assume "open S"
|
hoelzl@51343
|
338 |
then have "\<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. (\<Union>b\<in>B'. \<Inter>b) = S"
|
hoelzl@51343
|
339 |
unfolding B
|
hoelzl@51343
|
340 |
proof induct
|
wenzelm@53255
|
341 |
case UNIV
|
wenzelm@53255
|
342 |
show ?case by (intro exI[of _ "{{}}"]) simp
|
hoelzl@51343
|
343 |
next
|
hoelzl@51343
|
344 |
case (Int a b)
|
hoelzl@51343
|
345 |
then obtain x y where x: "a = UNION x Inter" "\<And>i. i \<in> x \<Longrightarrow> finite i \<and> i \<subseteq> B"
|
hoelzl@51343
|
346 |
and y: "b = UNION y Inter" "\<And>i. i \<in> y \<Longrightarrow> finite i \<and> i \<subseteq> B"
|
hoelzl@51343
|
347 |
by blast
|
hoelzl@51343
|
348 |
show ?case
|
hoelzl@51343
|
349 |
unfolding x y Int_UN_distrib2
|
hoelzl@51343
|
350 |
by (intro exI[of _ "{i \<union> j| i j. i \<in> x \<and> j \<in> y}"]) (auto dest: x(2) y(2))
|
hoelzl@51343
|
351 |
next
|
hoelzl@51343
|
352 |
case (UN K)
|
hoelzl@51343
|
353 |
then have "\<forall>k\<in>K. \<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. UNION B' Inter = k" by auto
|
wenzelm@55522
|
354 |
then obtain k where
|
wenzelm@55522
|
355 |
"\<forall>ka\<in>K. k ka \<subseteq> {b. finite b \<and> b \<subseteq> B} \<and> UNION (k ka) Inter = ka"
|
wenzelm@55522
|
356 |
unfolding bchoice_iff ..
|
hoelzl@51343
|
357 |
then show "\<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. UNION B' Inter = \<Union>K"
|
hoelzl@51343
|
358 |
by (intro exI[of _ "UNION K k"]) auto
|
hoelzl@51343
|
359 |
next
|
wenzelm@53255
|
360 |
case (Basis S)
|
wenzelm@53255
|
361 |
then show ?case
|
hoelzl@51343
|
362 |
by (intro exI[of _ "{{S}}"]) auto
|
hoelzl@51343
|
363 |
qed
|
hoelzl@51343
|
364 |
then have "(\<exists>B'\<subseteq>Inter ` {b. finite b \<and> b \<subseteq> B}. \<Union>B' = S)"
|
hoelzl@51343
|
365 |
unfolding subset_image_iff by blast }
|
hoelzl@51343
|
366 |
then show "topological_basis ?B"
|
hoelzl@51343
|
367 |
unfolding topological_space_class.topological_basis_def
|
wenzelm@53282
|
368 |
by (safe intro!: topological_space_class.open_Inter)
|
hoelzl@51343
|
369 |
(simp_all add: B generate_topology.Basis subset_eq)
|
hoelzl@51343
|
370 |
qed
|
hoelzl@51343
|
371 |
qed
|
hoelzl@51343
|
372 |
|
hoelzl@51343
|
373 |
end
|
hoelzl@51343
|
374 |
|
hoelzl@51343
|
375 |
sublocale second_countable_topology <
|
hoelzl@51343
|
376 |
countable_basis "SOME B. countable B \<and> topological_basis B"
|
hoelzl@51343
|
377 |
using someI_ex[OF ex_countable_basis]
|
hoelzl@51343
|
378 |
by unfold_locales safe
|
immler@50094
|
379 |
|
hoelzl@50882
|
380 |
instance prod :: (second_countable_topology, second_countable_topology) second_countable_topology
|
hoelzl@50882
|
381 |
proof
|
hoelzl@50882
|
382 |
obtain A :: "'a set set" where "countable A" "topological_basis A"
|
hoelzl@50882
|
383 |
using ex_countable_basis by auto
|
hoelzl@50882
|
384 |
moreover
|
hoelzl@50882
|
385 |
obtain B :: "'b set set" where "countable B" "topological_basis B"
|
hoelzl@50882
|
386 |
using ex_countable_basis by auto
|
hoelzl@51343
|
387 |
ultimately show "\<exists>B::('a \<times> 'b) set set. countable B \<and> open = generate_topology B"
|
hoelzl@51343
|
388 |
by (auto intro!: exI[of _ "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"] topological_basis_prod
|
hoelzl@51343
|
389 |
topological_basis_imp_subbasis)
|
hoelzl@50882
|
390 |
qed
|
hoelzl@50882
|
391 |
|
hoelzl@50883
|
392 |
instance second_countable_topology \<subseteq> first_countable_topology
|
hoelzl@50883
|
393 |
proof
|
hoelzl@50883
|
394 |
fix x :: 'a
|
hoelzl@50883
|
395 |
def B \<equiv> "SOME B::'a set set. countable B \<and> topological_basis B"
|
hoelzl@50883
|
396 |
then have B: "countable B" "topological_basis B"
|
hoelzl@50883
|
397 |
using countable_basis is_basis
|
hoelzl@50883
|
398 |
by (auto simp: countable_basis is_basis)
|
wenzelm@53282
|
399 |
then show "\<exists>A::nat \<Rightarrow> 'a set.
|
wenzelm@53282
|
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))"
|
hoelzl@51473
|
401 |
by (intro first_countableI[of "{b\<in>B. x \<in> b}"])
|
hoelzl@51473
|
402 |
(fastforce simp: topological_space_class.topological_basis_def)+
|
hoelzl@50883
|
403 |
qed
|
hoelzl@50883
|
404 |
|
wenzelm@53255
|
405 |
|
wenzelm@60420
|
406 |
subsection \<open>Polish spaces\<close>
|
wenzelm@60420
|
407 |
|
wenzelm@60420
|
408 |
text \<open>Textbooks define Polish spaces as completely metrizable.
|
wenzelm@60420
|
409 |
We assume the topology to be complete for a given metric.\<close>
|
immler@50087
|
410 |
|
hoelzl@50881
|
411 |
class polish_space = complete_space + second_countable_topology
|
immler@50087
|
412 |
|
wenzelm@60420
|
413 |
subsection \<open>General notion of a topology as a value\<close>
|
himmelma@33175
|
414 |
|
wenzelm@53255
|
415 |
definition "istopology L \<longleftrightarrow>
|
wenzelm@60585
|
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))"
|
wenzelm@53255
|
417 |
|
wenzelm@49834
|
418 |
typedef 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
|
himmelma@33175
|
419 |
morphisms "openin" "topology"
|
himmelma@33175
|
420 |
unfolding istopology_def by blast
|
himmelma@33175
|
421 |
|
himmelma@33175
|
422 |
lemma istopology_open_in[intro]: "istopology(openin U)"
|
himmelma@33175
|
423 |
using openin[of U] by blast
|
himmelma@33175
|
424 |
|
himmelma@33175
|
425 |
lemma topology_inverse': "istopology U \<Longrightarrow> openin (topology U) = U"
|
huffman@44170
|
426 |
using topology_inverse[unfolded mem_Collect_eq] .
|
himmelma@33175
|
427 |
|
himmelma@33175
|
428 |
lemma topology_inverse_iff: "istopology U \<longleftrightarrow> openin (topology U) = U"
|
himmelma@33175
|
429 |
using topology_inverse[of U] istopology_open_in[of "topology U"] by auto
|
himmelma@33175
|
430 |
|
himmelma@33175
|
431 |
lemma topology_eq: "T1 = T2 \<longleftrightarrow> (\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S)"
|
wenzelm@53255
|
432 |
proof
|
wenzelm@53255
|
433 |
assume "T1 = T2"
|
wenzelm@53255
|
434 |
then show "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S" by simp
|
wenzelm@53255
|
435 |
next
|
wenzelm@53255
|
436 |
assume H: "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S"
|
wenzelm@53255
|
437 |
then have "openin T1 = openin T2" by (simp add: fun_eq_iff)
|
wenzelm@53255
|
438 |
then have "topology (openin T1) = topology (openin T2)" by simp
|
wenzelm@53255
|
439 |
then show "T1 = T2" unfolding openin_inverse .
|
himmelma@33175
|
440 |
qed
|
himmelma@33175
|
441 |
|
wenzelm@60420
|
442 |
text\<open>Infer the "universe" from union of all sets in the topology.\<close>
|
himmelma@33175
|
443 |
|
wenzelm@53640
|
444 |
definition "topspace T = \<Union>{S. openin T S}"
|
himmelma@33175
|
445 |
|
wenzelm@60420
|
446 |
subsubsection \<open>Main properties of open sets\<close>
|
himmelma@33175
|
447 |
|
himmelma@33175
|
448 |
lemma openin_clauses:
|
himmelma@33175
|
449 |
fixes U :: "'a topology"
|
wenzelm@53282
|
450 |
shows
|
wenzelm@53282
|
451 |
"openin U {}"
|
wenzelm@53282
|
452 |
"\<And>S T. openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S\<inter>T)"
|
wenzelm@53282
|
453 |
"\<And>K. (\<forall>S \<in> K. openin U S) \<Longrightarrow> openin U (\<Union>K)"
|
wenzelm@53282
|
454 |
using openin[of U] unfolding istopology_def mem_Collect_eq by fast+
|
himmelma@33175
|
455 |
|
himmelma@33175
|
456 |
lemma openin_subset[intro]: "openin U S \<Longrightarrow> S \<subseteq> topspace U"
|
himmelma@33175
|
457 |
unfolding topspace_def by blast
|
wenzelm@53255
|
458 |
|
wenzelm@53255
|
459 |
lemma openin_empty[simp]: "openin U {}"
|
wenzelm@53255
|
460 |
by (simp add: openin_clauses)
|
himmelma@33175
|
461 |
|
himmelma@33175
|
462 |
lemma openin_Int[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<inter> T)"
|
huffman@36362
|
463 |
using openin_clauses by simp
|
huffman@36362
|
464 |
|
wenzelm@60585
|
465 |
lemma openin_Union[intro]: "(\<forall>S \<in>K. openin U S) \<Longrightarrow> openin U (\<Union>K)"
|
huffman@36362
|
466 |
using openin_clauses by simp
|
himmelma@33175
|
467 |
|
himmelma@33175
|
468 |
lemma openin_Un[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<union> T)"
|
himmelma@33175
|
469 |
using openin_Union[of "{S,T}" U] by auto
|
himmelma@33175
|
470 |
|
wenzelm@53255
|
471 |
lemma openin_topspace[intro, simp]: "openin U (topspace U)"
|
wenzelm@53255
|
472 |
by (simp add: openin_Union topspace_def)
|
himmelma@33175
|
473 |
|
wenzelm@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)"
|
wenzelm@49711
|
475 |
(is "?lhs \<longleftrightarrow> ?rhs")
|
huffman@36584
|
476 |
proof
|
wenzelm@49711
|
477 |
assume ?lhs
|
wenzelm@49711
|
478 |
then show ?rhs by auto
|
huffman@36584
|
479 |
next
|
huffman@36584
|
480 |
assume H: ?rhs
|
huffman@36584
|
481 |
let ?t = "\<Union>{T. openin U T \<and> T \<subseteq> S}"
|
huffman@36584
|
482 |
have "openin U ?t" by (simp add: openin_Union)
|
huffman@36584
|
483 |
also have "?t = S" using H by auto
|
huffman@36584
|
484 |
finally show "openin U S" .
|
himmelma@33175
|
485 |
qed
|
himmelma@33175
|
486 |
|
wenzelm@49711
|
487 |
|
wenzelm@60420
|
488 |
subsubsection \<open>Closed sets\<close>
|
himmelma@33175
|
489 |
|
himmelma@33175
|
490 |
definition "closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U - S)"
|
himmelma@33175
|
491 |
|
wenzelm@53255
|
492 |
lemma closedin_subset: "closedin U S \<Longrightarrow> S \<subseteq> topspace U"
|
wenzelm@53255
|
493 |
by (metis closedin_def)
|
wenzelm@53255
|
494 |
|
wenzelm@53255
|
495 |
lemma closedin_empty[simp]: "closedin U {}"
|
wenzelm@53255
|
496 |
by (simp add: closedin_def)
|
wenzelm@53255
|
497 |
|
wenzelm@53255
|
498 |
lemma closedin_topspace[intro, simp]: "closedin U (topspace U)"
|
wenzelm@53255
|
499 |
by (simp add: closedin_def)
|
wenzelm@53255
|
500 |
|
himmelma@33175
|
501 |
lemma closedin_Un[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<union> T)"
|
himmelma@33175
|
502 |
by (auto simp add: Diff_Un closedin_def)
|
himmelma@33175
|
503 |
|
wenzelm@60585
|
504 |
lemma Diff_Inter[intro]: "A - \<Inter>S = \<Union>{A - s|s. s\<in>S}"
|
wenzelm@53255
|
505 |
by auto
|
wenzelm@53255
|
506 |
|
wenzelm@53255
|
507 |
lemma closedin_Inter[intro]:
|
wenzelm@53255
|
508 |
assumes Ke: "K \<noteq> {}"
|
wenzelm@53255
|
509 |
and Kc: "\<forall>S \<in>K. closedin U S"
|
wenzelm@60585
|
510 |
shows "closedin U (\<Inter>K)"
|
wenzelm@53255
|
511 |
using Ke Kc unfolding closedin_def Diff_Inter by auto
|
himmelma@33175
|
512 |
|
himmelma@33175
|
513 |
lemma closedin_Int[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<inter> T)"
|
himmelma@33175
|
514 |
using closedin_Inter[of "{S,T}" U] by auto
|
himmelma@33175
|
515 |
|
himmelma@33175
|
516 |
lemma openin_closedin_eq: "openin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> closedin U (topspace U - S)"
|
himmelma@33175
|
517 |
apply (auto simp add: closedin_def Diff_Diff_Int inf_absorb2)
|
himmelma@33175
|
518 |
apply (metis openin_subset subset_eq)
|
himmelma@33175
|
519 |
done
|
himmelma@33175
|
520 |
|
wenzelm@53255
|
521 |
lemma openin_closedin: "S \<subseteq> topspace U \<Longrightarrow> (openin U S \<longleftrightarrow> closedin U (topspace U - S))"
|
himmelma@33175
|
522 |
by (simp add: openin_closedin_eq)
|
himmelma@33175
|
523 |
|
wenzelm@53255
|
524 |
lemma openin_diff[intro]:
|
wenzelm@53255
|
525 |
assumes oS: "openin U S"
|
wenzelm@53255
|
526 |
and cT: "closedin U T"
|
wenzelm@53255
|
527 |
shows "openin U (S - T)"
|
wenzelm@53255
|
528 |
proof -
|
himmelma@33175
|
529 |
have "S - T = S \<inter> (topspace U - T)" using openin_subset[of U S] oS cT
|
himmelma@33175
|
530 |
by (auto simp add: topspace_def openin_subset)
|
wenzelm@53282
|
531 |
then show ?thesis using oS cT
|
wenzelm@53282
|
532 |
by (auto simp add: closedin_def)
|
himmelma@33175
|
533 |
qed
|
himmelma@33175
|
534 |
|
wenzelm@53255
|
535 |
lemma closedin_diff[intro]:
|
wenzelm@53255
|
536 |
assumes oS: "closedin U S"
|
wenzelm@53255
|
537 |
and cT: "openin U T"
|
wenzelm@53255
|
538 |
shows "closedin U (S - T)"
|
wenzelm@53255
|
539 |
proof -
|
wenzelm@53255
|
540 |
have "S - T = S \<inter> (topspace U - T)"
|
wenzelm@53282
|
541 |
using closedin_subset[of U S] oS cT by (auto simp add: topspace_def)
|
wenzelm@53255
|
542 |
then show ?thesis
|
wenzelm@53255
|
543 |
using oS cT by (auto simp add: openin_closedin_eq)
|
wenzelm@53255
|
544 |
qed
|
wenzelm@53255
|
545 |
|
himmelma@33175
|
546 |
|
wenzelm@60420
|
547 |
subsubsection \<open>Subspace topology\<close>
|
huffman@44170
|
548 |
|
huffman@44170
|
549 |
definition "subtopology U V = topology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
|
huffman@44170
|
550 |
|
huffman@44170
|
551 |
lemma istopology_subtopology: "istopology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
|
huffman@44170
|
552 |
(is "istopology ?L")
|
wenzelm@53255
|
553 |
proof -
|
huffman@44170
|
554 |
have "?L {}" by blast
|
wenzelm@53255
|
555 |
{
|
wenzelm@53255
|
556 |
fix A B
|
wenzelm@53255
|
557 |
assume A: "?L A" and B: "?L B"
|
wenzelm@53255
|
558 |
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"
|
wenzelm@53255
|
559 |
by blast
|
wenzelm@53255
|
560 |
have "A \<inter> B = (Sa \<inter> Sb) \<inter> V" "openin U (Sa \<inter> Sb)"
|
wenzelm@53255
|
561 |
using Sa Sb by blast+
|
wenzelm@53255
|
562 |
then have "?L (A \<inter> B)" by blast
|
wenzelm@53255
|
563 |
}
|
himmelma@33175
|
564 |
moreover
|
wenzelm@53255
|
565 |
{
|
wenzelm@53282
|
566 |
fix K
|
wenzelm@53282
|
567 |
assume K: "K \<subseteq> Collect ?L"
|
huffman@44170
|
568 |
have th0: "Collect ?L = (\<lambda>S. S \<inter> V) ` Collect (openin U)"
|
lp15@55775
|
569 |
by blast
|
himmelma@33175
|
570 |
from K[unfolded th0 subset_image_iff]
|
wenzelm@53255
|
571 |
obtain Sk where Sk: "Sk \<subseteq> Collect (openin U)" "K = (\<lambda>S. S \<inter> V) ` Sk"
|
wenzelm@53255
|
572 |
by blast
|
wenzelm@53255
|
573 |
have "\<Union>K = (\<Union>Sk) \<inter> V"
|
wenzelm@53255
|
574 |
using Sk by auto
|
wenzelm@60585
|
575 |
moreover have "openin U (\<Union>Sk)"
|
wenzelm@53255
|
576 |
using Sk by (auto simp add: subset_eq)
|
wenzelm@53255
|
577 |
ultimately have "?L (\<Union>K)" by blast
|
wenzelm@53255
|
578 |
}
|
huffman@44170
|
579 |
ultimately show ?thesis
|
huffman@44170
|
580 |
unfolding subset_eq mem_Collect_eq istopology_def by blast
|
himmelma@33175
|
581 |
qed
|
himmelma@33175
|
582 |
|
wenzelm@53255
|
583 |
lemma openin_subtopology: "openin (subtopology U V) S \<longleftrightarrow> (\<exists>T. openin U T \<and> S = T \<inter> V)"
|
himmelma@33175
|
584 |
unfolding subtopology_def topology_inverse'[OF istopology_subtopology]
|
huffman@44170
|
585 |
by auto
|
himmelma@33175
|
586 |
|
wenzelm@53255
|
587 |
lemma topspace_subtopology: "topspace (subtopology U V) = topspace U \<inter> V"
|
himmelma@33175
|
588 |
by (auto simp add: topspace_def openin_subtopology)
|
himmelma@33175
|
589 |
|
wenzelm@53255
|
590 |
lemma closedin_subtopology: "closedin (subtopology U V) S \<longleftrightarrow> (\<exists>T. closedin U T \<and> S = T \<inter> V)"
|
himmelma@33175
|
591 |
unfolding closedin_def topspace_subtopology
|
lp15@55775
|
592 |
by (auto simp add: openin_subtopology)
|
himmelma@33175
|
593 |
|
himmelma@33175
|
594 |
lemma openin_subtopology_refl: "openin (subtopology U V) V \<longleftrightarrow> V \<subseteq> topspace U"
|
himmelma@33175
|
595 |
unfolding openin_subtopology
|
lp15@55775
|
596 |
by auto (metis IntD1 in_mono openin_subset)
|
wenzelm@49711
|
597 |
|
wenzelm@49711
|
598 |
lemma subtopology_superset:
|
wenzelm@49711
|
599 |
assumes UV: "topspace U \<subseteq> V"
|
himmelma@33175
|
600 |
shows "subtopology U V = U"
|
wenzelm@53255
|
601 |
proof -
|
wenzelm@53255
|
602 |
{
|
wenzelm@53255
|
603 |
fix S
|
wenzelm@53255
|
604 |
{
|
wenzelm@53255
|
605 |
fix T
|
wenzelm@53255
|
606 |
assume T: "openin U T" "S = T \<inter> V"
|
wenzelm@53255
|
607 |
from T openin_subset[OF T(1)] UV have eq: "S = T"
|
wenzelm@53255
|
608 |
by blast
|
wenzelm@53255
|
609 |
have "openin U S"
|
wenzelm@53255
|
610 |
unfolding eq using T by blast
|
wenzelm@53255
|
611 |
}
|
himmelma@33175
|
612 |
moreover
|
wenzelm@53255
|
613 |
{
|
wenzelm@53255
|
614 |
assume S: "openin U S"
|
wenzelm@53255
|
615 |
then have "\<exists>T. openin U T \<and> S = T \<inter> V"
|
wenzelm@53255
|
616 |
using openin_subset[OF S] UV by auto
|
wenzelm@53255
|
617 |
}
|
wenzelm@53255
|
618 |
ultimately have "(\<exists>T. openin U T \<and> S = T \<inter> V) \<longleftrightarrow> openin U S"
|
wenzelm@53255
|
619 |
by blast
|
wenzelm@53255
|
620 |
}
|
wenzelm@53255
|
621 |
then show ?thesis
|
wenzelm@53255
|
622 |
unfolding topology_eq openin_subtopology by blast
|
himmelma@33175
|
623 |
qed
|
himmelma@33175
|
624 |
|
himmelma@33175
|
625 |
lemma subtopology_topspace[simp]: "subtopology U (topspace U) = U"
|
himmelma@33175
|
626 |
by (simp add: subtopology_superset)
|
himmelma@33175
|
627 |
|
himmelma@33175
|
628 |
lemma subtopology_UNIV[simp]: "subtopology U UNIV = U"
|
himmelma@33175
|
629 |
by (simp add: subtopology_superset)
|
himmelma@33175
|
630 |
|
wenzelm@53255
|
631 |
|
wenzelm@60420
|
632 |
subsubsection \<open>The standard Euclidean topology\<close>
|
himmelma@33175
|
633 |
|
wenzelm@53255
|
634 |
definition euclidean :: "'a::topological_space topology"
|
wenzelm@53255
|
635 |
where "euclidean = topology open"
|
himmelma@33175
|
636 |
|
himmelma@33175
|
637 |
lemma open_openin: "open S \<longleftrightarrow> openin euclidean S"
|
himmelma@33175
|
638 |
unfolding euclidean_def
|
himmelma@33175
|
639 |
apply (rule cong[where x=S and y=S])
|
himmelma@33175
|
640 |
apply (rule topology_inverse[symmetric])
|
himmelma@33175
|
641 |
apply (auto simp add: istopology_def)
|
huffman@44170
|
642 |
done
|
himmelma@33175
|
643 |
|
himmelma@33175
|
644 |
lemma topspace_euclidean: "topspace euclidean = UNIV"
|
himmelma@33175
|
645 |
apply (simp add: topspace_def)
|
nipkow@39302
|
646 |
apply (rule set_eqI)
|
wenzelm@53255
|
647 |
apply (auto simp add: open_openin[symmetric])
|
wenzelm@53255
|
648 |
done
|
himmelma@33175
|
649 |
|
himmelma@33175
|
650 |
lemma topspace_euclidean_subtopology[simp]: "topspace (subtopology euclidean S) = S"
|
himmelma@33175
|
651 |
by (simp add: topspace_euclidean topspace_subtopology)
|
himmelma@33175
|
652 |
|
himmelma@33175
|
653 |
lemma closed_closedin: "closed S \<longleftrightarrow> closedin euclidean S"
|
himmelma@33175
|
654 |
by (simp add: closed_def closedin_def topspace_euclidean open_openin Compl_eq_Diff_UNIV)
|
himmelma@33175
|
655 |
|
himmelma@33175
|
656 |
lemma open_subopen: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S)"
|
himmelma@33175
|
657 |
by (simp add: open_openin openin_subopen[symmetric])
|
himmelma@33175
|
658 |
|
wenzelm@60420
|
659 |
text \<open>Basic "localization" results are handy for connectedness.\<close>
|
huffman@44210
|
660 |
|
huffman@44210
|
661 |
lemma openin_open: "openin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. open T \<and> (S = U \<inter> T))"
|
huffman@44210
|
662 |
by (auto simp add: openin_subtopology open_openin[symmetric])
|
huffman@44210
|
663 |
|
huffman@44210
|
664 |
lemma openin_open_Int[intro]: "open S \<Longrightarrow> openin (subtopology euclidean U) (U \<inter> S)"
|
huffman@44210
|
665 |
by (auto simp add: openin_open)
|
huffman@44210
|
666 |
|
huffman@44210
|
667 |
lemma open_openin_trans[trans]:
|
wenzelm@53255
|
668 |
"open S \<Longrightarrow> open T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> openin (subtopology euclidean S) T"
|
huffman@44210
|
669 |
by (metis Int_absorb1 openin_open_Int)
|
huffman@44210
|
670 |
|
wenzelm@53255
|
671 |
lemma open_subset: "S \<subseteq> T \<Longrightarrow> open S \<Longrightarrow> openin (subtopology euclidean T) S"
|
huffman@44210
|
672 |
by (auto simp add: openin_open)
|
huffman@44210
|
673 |
|
huffman@44210
|
674 |
lemma closedin_closed: "closedin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. closed T \<and> S = U \<inter> T)"
|
huffman@44210
|
675 |
by (simp add: closedin_subtopology closed_closedin Int_ac)
|
huffman@44210
|
676 |
|
wenzelm@53291
|
677 |
lemma closedin_closed_Int: "closed S \<Longrightarrow> closedin (subtopology euclidean U) (U \<inter> S)"
|
huffman@44210
|
678 |
by (metis closedin_closed)
|
huffman@44210
|
679 |
|
wenzelm@53282
|
680 |
lemma closed_closedin_trans:
|
wenzelm@53282
|
681 |
"closed S \<Longrightarrow> closed T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> closedin (subtopology euclidean S) T"
|
lp15@55775
|
682 |
by (metis closedin_closed inf.absorb2)
|
huffman@44210
|
683 |
|
huffman@44210
|
684 |
lemma closed_subset: "S \<subseteq> T \<Longrightarrow> closed S \<Longrightarrow> closedin (subtopology euclidean T) S"
|
huffman@44210
|
685 |
by (auto simp add: closedin_closed)
|
huffman@44210
|
686 |
|
huffman@44210
|
687 |
lemma openin_euclidean_subtopology_iff:
|
huffman@44210
|
688 |
fixes S U :: "'a::metric_space set"
|
wenzelm@53255
|
689 |
shows "openin (subtopology euclidean U) S \<longleftrightarrow>
|
wenzelm@53255
|
690 |
S \<subseteq> U \<and> (\<forall>x\<in>S. \<exists>e>0. \<forall>x'\<in>U. dist x' x < e \<longrightarrow> x'\<in> S)"
|
wenzelm@53255
|
691 |
(is "?lhs \<longleftrightarrow> ?rhs")
|
huffman@44210
|
692 |
proof
|
wenzelm@53255
|
693 |
assume ?lhs
|
wenzelm@53282
|
694 |
then show ?rhs
|
wenzelm@53282
|
695 |
unfolding openin_open open_dist by blast
|
huffman@44210
|
696 |
next
|
huffman@44210
|
697 |
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}"
|
huffman@44210
|
698 |
have 1: "\<forall>x\<in>T. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> T"
|
huffman@44210
|
699 |
unfolding T_def
|
huffman@44210
|
700 |
apply clarsimp
|
huffman@44210
|
701 |
apply (rule_tac x="d - dist x a" in exI)
|
huffman@44210
|
702 |
apply (clarsimp simp add: less_diff_eq)
|
lp15@55775
|
703 |
by (metis dist_commute dist_triangle_lt)
|
wenzelm@53282
|
704 |
assume ?rhs then have 2: "S = U \<inter> T"
|
lp15@60141
|
705 |
unfolding T_def
|
lp15@55775
|
706 |
by auto (metis dist_self)
|
huffman@44210
|
707 |
from 1 2 show ?lhs
|
huffman@44210
|
708 |
unfolding openin_open open_dist by fast
|
huffman@44210
|
709 |
qed
|
lp15@61609
|
710 |
|
lp15@61306
|
711 |
lemma connected_open_in:
|
lp15@61306
|
712 |
"connected s \<longleftrightarrow>
|
lp15@61306
|
713 |
~(\<exists>e1 e2. openin (subtopology euclidean s) e1 \<and>
|
lp15@61306
|
714 |
openin (subtopology euclidean s) e2 \<and>
|
lp15@61306
|
715 |
s \<subseteq> e1 \<union> e2 \<and> e1 \<inter> e2 = {} \<and> e1 \<noteq> {} \<and> e2 \<noteq> {})"
|
lp15@61306
|
716 |
apply (simp add: connected_def openin_open, safe)
|
lp15@61609
|
717 |
apply (simp_all, blast+) --\<open>slow\<close>
|
lp15@61306
|
718 |
done
|
lp15@61306
|
719 |
|
lp15@61306
|
720 |
lemma connected_open_in_eq:
|
lp15@61306
|
721 |
"connected s \<longleftrightarrow>
|
lp15@61306
|
722 |
~(\<exists>e1 e2. openin (subtopology euclidean s) e1 \<and>
|
lp15@61306
|
723 |
openin (subtopology euclidean s) e2 \<and>
|
lp15@61306
|
724 |
e1 \<union> e2 = s \<and> e1 \<inter> e2 = {} \<and>
|
lp15@61306
|
725 |
e1 \<noteq> {} \<and> e2 \<noteq> {})"
|
lp15@61306
|
726 |
apply (simp add: connected_open_in, safe)
|
lp15@61306
|
727 |
apply blast
|
lp15@61306
|
728 |
by (metis Int_lower1 Un_subset_iff openin_open subset_antisym)
|
lp15@61306
|
729 |
|
lp15@61306
|
730 |
lemma connected_closed_in:
|
lp15@61306
|
731 |
"connected s \<longleftrightarrow>
|
lp15@61306
|
732 |
~(\<exists>e1 e2.
|
lp15@61306
|
733 |
closedin (subtopology euclidean s) e1 \<and>
|
lp15@61306
|
734 |
closedin (subtopology euclidean s) e2 \<and>
|
lp15@61306
|
735 |
s \<subseteq> e1 \<union> e2 \<and> e1 \<inter> e2 = {} \<and>
|
lp15@61306
|
736 |
e1 \<noteq> {} \<and> e2 \<noteq> {})"
|
lp15@61306
|
737 |
proof -
|
lp15@61306
|
738 |
{ fix A B x x'
|
lp15@61306
|
739 |
assume s_sub: "s \<subseteq> A \<union> B"
|
lp15@61306
|
740 |
and disj: "A \<inter> B \<inter> s = {}"
|
lp15@61306
|
741 |
and x: "x \<in> s" "x \<in> B" and x': "x' \<in> s" "x' \<in> A"
|
lp15@61306
|
742 |
and cl: "closed A" "closed B"
|
lp15@61306
|
743 |
assume "\<forall>e1. (\<forall>T. closed T \<longrightarrow> e1 \<noteq> s \<inter> T) \<or> (\<forall>e2. e1 \<inter> e2 = {} \<longrightarrow> s \<subseteq> e1 \<union> e2 \<longrightarrow> (\<forall>T. closed T \<longrightarrow> e2 \<noteq> s \<inter> T) \<or> e1 = {} \<or> e2 = {})"
|
lp15@61306
|
744 |
then have "\<And>C D. s \<inter> C = {} \<or> s \<inter> D = {} \<or> s \<inter> (C \<inter> (s \<inter> D)) \<noteq> {} \<or> \<not> s \<subseteq> s \<inter> (C \<union> D) \<or> \<not> closed C \<or> \<not> closed D"
|
lp15@61306
|
745 |
by (metis (no_types) Int_Un_distrib Int_assoc)
|
lp15@61306
|
746 |
moreover have "s \<inter> (A \<inter> B) = {}" "s \<inter> (A \<union> B) = s" "s \<inter> B \<noteq> {}"
|
lp15@61306
|
747 |
using disj s_sub x by blast+
|
lp15@61306
|
748 |
ultimately have "s \<inter> A = {}"
|
lp15@61306
|
749 |
using cl by (metis inf.left_commute inf_bot_right order_refl)
|
lp15@61306
|
750 |
then have False
|
lp15@61306
|
751 |
using x' by blast
|
lp15@61306
|
752 |
} note * = this
|
lp15@61306
|
753 |
show ?thesis
|
lp15@61306
|
754 |
apply (simp add: connected_closed closedin_closed)
|
lp15@61306
|
755 |
apply (safe; simp)
|
lp15@61306
|
756 |
apply blast
|
lp15@61306
|
757 |
apply (blast intro: *)
|
lp15@61306
|
758 |
done
|
lp15@61306
|
759 |
qed
|
lp15@61306
|
760 |
|
lp15@61306
|
761 |
lemma connected_closed_in_eq:
|
lp15@61306
|
762 |
"connected s \<longleftrightarrow>
|
lp15@61306
|
763 |
~(\<exists>e1 e2.
|
lp15@61306
|
764 |
closedin (subtopology euclidean s) e1 \<and>
|
lp15@61306
|
765 |
closedin (subtopology euclidean s) e2 \<and>
|
lp15@61306
|
766 |
e1 \<union> e2 = s \<and> e1 \<inter> e2 = {} \<and>
|
lp15@61306
|
767 |
e1 \<noteq> {} \<and> e2 \<noteq> {})"
|
lp15@61306
|
768 |
apply (simp add: connected_closed_in, safe)
|
lp15@61306
|
769 |
apply blast
|
lp15@61306
|
770 |
by (metis Int_lower1 Un_subset_iff closedin_closed subset_antisym)
|
lp15@61609
|
771 |
|
wenzelm@60420
|
772 |
text \<open>These "transitivity" results are handy too\<close>
|
huffman@44210
|
773 |
|
wenzelm@53255
|
774 |
lemma openin_trans[trans]:
|
wenzelm@53255
|
775 |
"openin (subtopology euclidean T) S \<Longrightarrow> openin (subtopology euclidean U) T \<Longrightarrow>
|
wenzelm@53255
|
776 |
openin (subtopology euclidean U) S"
|
huffman@44210
|
777 |
unfolding open_openin openin_open by blast
|
huffman@44210
|
778 |
|
huffman@44210
|
779 |
lemma openin_open_trans: "openin (subtopology euclidean T) S \<Longrightarrow> open T \<Longrightarrow> open S"
|
huffman@44210
|
780 |
by (auto simp add: openin_open intro: openin_trans)
|
huffman@44210
|
781 |
|
huffman@44210
|
782 |
lemma closedin_trans[trans]:
|
wenzelm@53255
|
783 |
"closedin (subtopology euclidean T) S \<Longrightarrow> closedin (subtopology euclidean U) T \<Longrightarrow>
|
wenzelm@53255
|
784 |
closedin (subtopology euclidean U) S"
|
huffman@44210
|
785 |
by (auto simp add: closedin_closed closed_closedin closed_Inter Int_assoc)
|
huffman@44210
|
786 |
|
huffman@44210
|
787 |
lemma closedin_closed_trans: "closedin (subtopology euclidean T) S \<Longrightarrow> closed T \<Longrightarrow> closed S"
|
huffman@44210
|
788 |
by (auto simp add: closedin_closed intro: closedin_trans)
|
huffman@44210
|
789 |
|
paulson@61518
|
790 |
lemma openin_subtopology_inter_subset:
|
paulson@61518
|
791 |
"openin (subtopology euclidean u) (u \<inter> s) \<and> v \<subseteq> u \<Longrightarrow> openin (subtopology euclidean v) (v \<inter> s)"
|
paulson@61518
|
792 |
by (auto simp: openin_subtopology)
|
paulson@61518
|
793 |
|
paulson@61518
|
794 |
lemma openin_open_eq: "open s \<Longrightarrow> (openin (subtopology euclidean s) t \<longleftrightarrow> open t \<and> t \<subseteq> s)"
|
paulson@61518
|
795 |
using open_subset openin_open_trans openin_subset by fastforce
|
paulson@61518
|
796 |
|
huffman@44210
|
797 |
|
wenzelm@60420
|
798 |
subsection \<open>Open and closed balls\<close>
|
himmelma@33175
|
799 |
|
wenzelm@53255
|
800 |
definition ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
|
wenzelm@53255
|
801 |
where "ball x e = {y. dist x y < e}"
|
wenzelm@53255
|
802 |
|
wenzelm@53255
|
803 |
definition cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
|
wenzelm@53255
|
804 |
where "cball x e = {y. dist x y \<le> e}"
|
himmelma@33175
|
805 |
|
huffman@45776
|
806 |
lemma mem_ball [simp]: "y \<in> ball x e \<longleftrightarrow> dist x y < e"
|
huffman@45776
|
807 |
by (simp add: ball_def)
|
huffman@45776
|
808 |
|
huffman@45776
|
809 |
lemma mem_cball [simp]: "y \<in> cball x e \<longleftrightarrow> dist x y \<le> e"
|
huffman@45776
|
810 |
by (simp add: cball_def)
|
huffman@45776
|
811 |
|
paulson@61518
|
812 |
lemma ball_trivial [simp]: "ball x 0 = {}"
|
paulson@61518
|
813 |
by (simp add: ball_def)
|
paulson@61518
|
814 |
|
paulson@61518
|
815 |
lemma cball_trivial [simp]: "cball x 0 = {x}"
|
paulson@61518
|
816 |
by (simp add: cball_def)
|
paulson@61518
|
817 |
|
paulson@61518
|
818 |
lemma mem_ball_0 [simp]:
|
himmelma@33175
|
819 |
fixes x :: "'a::real_normed_vector"
|
himmelma@33175
|
820 |
shows "x \<in> ball 0 e \<longleftrightarrow> norm x < e"
|
himmelma@33175
|
821 |
by (simp add: dist_norm)
|
himmelma@33175
|
822 |
|
paulson@61518
|
823 |
lemma mem_cball_0 [simp]:
|
himmelma@33175
|
824 |
fixes x :: "'a::real_normed_vector"
|
himmelma@33175
|
825 |
shows "x \<in> cball 0 e \<longleftrightarrow> norm x \<le> e"
|
himmelma@33175
|
826 |
by (simp add: dist_norm)
|
himmelma@33175
|
827 |
|
paulson@61518
|
828 |
lemma centre_in_ball [simp]: "x \<in> ball x e \<longleftrightarrow> 0 < e"
|
huffman@45776
|
829 |
by simp
|
huffman@45776
|
830 |
|
paulson@61518
|
831 |
lemma centre_in_cball [simp]: "x \<in> cball x e \<longleftrightarrow> 0 \<le> e"
|
huffman@45776
|
832 |
by simp
|
huffman@45776
|
833 |
|
paulson@61518
|
834 |
lemma ball_subset_cball [simp,intro]: "ball x e \<subseteq> cball x e"
|
wenzelm@53255
|
835 |
by (simp add: subset_eq)
|
wenzelm@53255
|
836 |
|
wenzelm@53282
|
837 |
lemma subset_ball[intro]: "d \<le> e \<Longrightarrow> ball x d \<subseteq> ball x e"
|
wenzelm@53255
|
838 |
by (simp add: subset_eq)
|
wenzelm@53255
|
839 |
|
wenzelm@53282
|
840 |
lemma subset_cball[intro]: "d \<le> e \<Longrightarrow> cball x d \<subseteq> cball x e"
|
wenzelm@53255
|
841 |
by (simp add: subset_eq)
|
wenzelm@53255
|
842 |
|
himmelma@33175
|
843 |
lemma ball_max_Un: "ball a (max r s) = ball a r \<union> ball a s"
|
nipkow@39302
|
844 |
by (simp add: set_eq_iff) arith
|
himmelma@33175
|
845 |
|
himmelma@33175
|
846 |
lemma ball_min_Int: "ball a (min r s) = ball a r \<inter> ball a s"
|
nipkow@39302
|
847 |
by (simp add: set_eq_iff)
|
himmelma@33175
|
848 |
|
lp15@61426
|
849 |
lemma cball_diff_eq_sphere: "cball a r - ball a r = {x. dist x a = r}"
|
lp15@61426
|
850 |
by (auto simp: cball_def ball_def dist_commute)
|
lp15@61426
|
851 |
|
wenzelm@53255
|
852 |
lemma diff_less_iff:
|
wenzelm@53255
|
853 |
"(a::real) - b > 0 \<longleftrightarrow> a > b"
|
himmelma@33175
|
854 |
"(a::real) - b < 0 \<longleftrightarrow> a < b"
|
wenzelm@53255
|
855 |
"a - b < c \<longleftrightarrow> a < c + b" "a - b > c \<longleftrightarrow> a > c + b"
|
wenzelm@53255
|
856 |
by arith+
|
wenzelm@53255
|
857 |
|
wenzelm@53255
|
858 |
lemma diff_le_iff:
|
wenzelm@53255
|
859 |
"(a::real) - b \<ge> 0 \<longleftrightarrow> a \<ge> b"
|
wenzelm@53255
|
860 |
"(a::real) - b \<le> 0 \<longleftrightarrow> a \<le> b"
|
wenzelm@53255
|
861 |
"a - b \<le> c \<longleftrightarrow> a \<le> c + b"
|
wenzelm@53255
|
862 |
"a - b \<ge> c \<longleftrightarrow> a \<ge> c + b"
|
wenzelm@53255
|
863 |
by arith+
|
himmelma@33175
|
864 |
|
huffman@54070
|
865 |
lemma open_ball [intro, simp]: "open (ball x e)"
|
huffman@54070
|
866 |
proof -
|
huffman@54070
|
867 |
have "open (dist x -` {..<e})"
|
hoelzl@56371
|
868 |
by (intro open_vimage open_lessThan continuous_intros)
|
huffman@54070
|
869 |
also have "dist x -` {..<e} = ball x e"
|
huffman@54070
|
870 |
by auto
|
huffman@54070
|
871 |
finally show ?thesis .
|
huffman@54070
|
872 |
qed
|
himmelma@33175
|
873 |
|
himmelma@33175
|
874 |
lemma open_contains_ball: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. ball x e \<subseteq> S)"
|
himmelma@33175
|
875 |
unfolding open_dist subset_eq mem_ball Ball_def dist_commute ..
|
himmelma@33175
|
876 |
|
hoelzl@33714
|
877 |
lemma openE[elim?]:
|
wenzelm@53282
|
878 |
assumes "open S" "x\<in>S"
|
hoelzl@33714
|
879 |
obtains e where "e>0" "ball x e \<subseteq> S"
|
hoelzl@33714
|
880 |
using assms unfolding open_contains_ball by auto
|
hoelzl@33714
|
881 |
|
himmelma@33175
|
882 |
lemma open_contains_ball_eq: "open S \<Longrightarrow> \<forall>x. x\<in>S \<longleftrightarrow> (\<exists>e>0. ball x e \<subseteq> S)"
|
himmelma@33175
|
883 |
by (metis open_contains_ball subset_eq centre_in_ball)
|
himmelma@33175
|
884 |
|
himmelma@33175
|
885 |
lemma ball_eq_empty[simp]: "ball x e = {} \<longleftrightarrow> e \<le> 0"
|
nipkow@39302
|
886 |
unfolding mem_ball set_eq_iff
|
himmelma@33175
|
887 |
apply (simp add: not_less)
|
wenzelm@52624
|
888 |
apply (metis zero_le_dist order_trans dist_self)
|
wenzelm@52624
|
889 |
done
|
himmelma@33175
|
890 |
|
lp15@61694
|
891 |
lemma ball_empty: "e \<le> 0 \<Longrightarrow> ball x e = {}" by simp
|
himmelma@33175
|
892 |
|
hoelzl@50526
|
893 |
lemma euclidean_dist_l2:
|
hoelzl@50526
|
894 |
fixes x y :: "'a :: euclidean_space"
|
hoelzl@50526
|
895 |
shows "dist x y = setL2 (\<lambda>i. dist (x \<bullet> i) (y \<bullet> i)) Basis"
|
hoelzl@50526
|
896 |
unfolding dist_norm norm_eq_sqrt_inner setL2_def
|
hoelzl@50526
|
897 |
by (subst euclidean_inner) (simp add: power2_eq_square inner_diff_left)
|
hoelzl@50526
|
898 |
|
eberlm@61531
|
899 |
lemma eventually_nhds_ball: "d > 0 \<Longrightarrow> eventually (\<lambda>x. x \<in> ball z d) (nhds z)"
|
eberlm@61531
|
900 |
by (rule eventually_nhds_in_open) simp_all
|
eberlm@61531
|
901 |
|
eberlm@61531
|
902 |
lemma eventually_at_ball: "d > 0 \<Longrightarrow> eventually (\<lambda>t. t \<in> ball z d \<and> t \<in> A) (at z within A)"
|
eberlm@61531
|
903 |
unfolding eventually_at by (intro exI[of _ d]) (simp_all add: dist_commute)
|
eberlm@61531
|
904 |
|
eberlm@61531
|
905 |
lemma eventually_at_ball': "d > 0 \<Longrightarrow> eventually (\<lambda>t. t \<in> ball z d \<and> t \<noteq> z \<and> t \<in> A) (at z within A)"
|
eberlm@61531
|
906 |
unfolding eventually_at by (intro exI[of _ d]) (simp_all add: dist_commute)
|
eberlm@61531
|
907 |
|
immler@56189
|
908 |
|
wenzelm@60420
|
909 |
subsection \<open>Boxes\<close>
|
immler@56189
|
910 |
|
hoelzl@57447
|
911 |
abbreviation One :: "'a::euclidean_space"
|
hoelzl@57447
|
912 |
where "One \<equiv> \<Sum>Basis"
|
hoelzl@57447
|
913 |
|
immler@54775
|
914 |
definition (in euclidean_space) eucl_less (infix "<e" 50)
|
immler@54775
|
915 |
where "eucl_less a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i)"
|
immler@54775
|
916 |
|
immler@54775
|
917 |
definition box_eucl_less: "box a b = {x. a <e x \<and> x <e b}"
|
immler@56188
|
918 |
definition "cbox a b = {x. \<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i}"
|
immler@54775
|
919 |
|
immler@54775
|
920 |
lemma box_def: "box a b = {x. \<forall>i\<in>Basis. a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i}"
|
immler@54775
|
921 |
and in_box_eucl_less: "x \<in> box a b \<longleftrightarrow> a <e x \<and> x <e b"
|
immler@56188
|
922 |
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)"
|
immler@56188
|
923 |
"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)"
|
immler@56188
|
924 |
by (auto simp: box_eucl_less eucl_less_def cbox_def)
|
immler@56188
|
925 |
|
lp15@60615
|
926 |
lemma cbox_Pair_eq: "cbox (a, c) (b, d) = cbox a b \<times> cbox c d"
|
lp15@60615
|
927 |
by (force simp: cbox_def Basis_prod_def)
|
lp15@60615
|
928 |
|
lp15@60615
|
929 |
lemma cbox_Pair_iff [iff]: "(x, y) \<in> cbox (a, c) (b, d) \<longleftrightarrow> x \<in> cbox a b \<and> y \<in> cbox c d"
|
lp15@60615
|
930 |
by (force simp: cbox_Pair_eq)
|
lp15@60615
|
931 |
|
lp15@60615
|
932 |
lemma cbox_Pair_eq_0: "cbox (a, c) (b, d) = {} \<longleftrightarrow> cbox a b = {} \<or> cbox c d = {}"
|
lp15@60615
|
933 |
by (force simp: cbox_Pair_eq)
|
lp15@60615
|
934 |
|
lp15@60615
|
935 |
lemma swap_cbox_Pair [simp]: "prod.swap ` cbox (c, a) (d, b) = cbox (a,c) (b,d)"
|
lp15@60615
|
936 |
by auto
|
lp15@60615
|
937 |
|
immler@56188
|
938 |
lemma mem_box_real[simp]:
|
immler@56188
|
939 |
"(x::real) \<in> box a b \<longleftrightarrow> a < x \<and> x < b"
|
immler@56188
|
940 |
"(x::real) \<in> cbox a b \<longleftrightarrow> a \<le> x \<and> x \<le> b"
|
immler@56188
|
941 |
by (auto simp: mem_box)
|
immler@56188
|
942 |
|
immler@56188
|
943 |
lemma box_real[simp]:
|
immler@56188
|
944 |
fixes a b:: real
|
immler@56188
|
945 |
shows "box a b = {a <..< b}" "cbox a b = {a .. b}"
|
immler@56188
|
946 |
by auto
|
hoelzl@50526
|
947 |
|
hoelzl@57447
|
948 |
lemma box_Int_box:
|
hoelzl@57447
|
949 |
fixes a :: "'a::euclidean_space"
|
hoelzl@57447
|
950 |
shows "box a b \<inter> box c d =
|
hoelzl@57447
|
951 |
box (\<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)"
|
hoelzl@57447
|
952 |
unfolding set_eq_iff and Int_iff and mem_box by auto
|
hoelzl@57447
|
953 |
|
immler@50087
|
954 |
lemma rational_boxes:
|
wenzelm@61076
|
955 |
fixes x :: "'a::euclidean_space"
|
wenzelm@53291
|
956 |
assumes "e > 0"
|
hoelzl@50526
|
957 |
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"
|
immler@50087
|
958 |
proof -
|
immler@50087
|
959 |
def e' \<equiv> "e / (2 * sqrt (real (DIM ('a))))"
|
wenzelm@53291
|
960 |
then have e: "e' > 0"
|
nipkow@56541
|
961 |
using assms by (auto simp: DIM_positive)
|
hoelzl@50526
|
962 |
have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x \<bullet> i \<and> x \<bullet> i - y < e'" (is "\<forall>i. ?th i")
|
immler@50087
|
963 |
proof
|
wenzelm@53255
|
964 |
fix i
|
wenzelm@53255
|
965 |
from Rats_dense_in_real[of "x \<bullet> i - e'" "x \<bullet> i"] e
|
wenzelm@53255
|
966 |
show "?th i" by auto
|
immler@50087
|
967 |
qed
|
wenzelm@55522
|
968 |
from choice[OF this] obtain a where
|
wenzelm@55522
|
969 |
a: "\<forall>xa. a xa \<in> \<rat> \<and> a xa < x \<bullet> xa \<and> x \<bullet> xa - a xa < e'" ..
|
hoelzl@50526
|
970 |
have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x \<bullet> i < y \<and> y - x \<bullet> i < e'" (is "\<forall>i. ?th i")
|
immler@50087
|
971 |
proof
|
wenzelm@53255
|
972 |
fix i
|
wenzelm@53255
|
973 |
from Rats_dense_in_real[of "x \<bullet> i" "x \<bullet> i + e'"] e
|
wenzelm@53255
|
974 |
show "?th i" by auto
|
immler@50087
|
975 |
qed
|
wenzelm@55522
|
976 |
from choice[OF this] obtain b where
|
wenzelm@55522
|
977 |
b: "\<forall>xa. b xa \<in> \<rat> \<and> x \<bullet> xa < b xa \<and> b xa - x \<bullet> xa < e'" ..
|
hoelzl@50526
|
978 |
let ?a = "\<Sum>i\<in>Basis. a i *\<^sub>R i" and ?b = "\<Sum>i\<in>Basis. b i *\<^sub>R i"
|
hoelzl@50526
|
979 |
show ?thesis
|
hoelzl@50526
|
980 |
proof (rule exI[of _ ?a], rule exI[of _ ?b], safe)
|
wenzelm@53255
|
981 |
fix y :: 'a
|
wenzelm@53255
|
982 |
assume *: "y \<in> box ?a ?b"
|
wenzelm@53015
|
983 |
have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)"
|
immler@50087
|
984 |
unfolding setL2_def[symmetric] by (rule euclidean_dist_l2)
|
hoelzl@50526
|
985 |
also have "\<dots> < sqrt (\<Sum>(i::'a)\<in>Basis. e^2 / real (DIM('a)))"
|
immler@50087
|
986 |
proof (rule real_sqrt_less_mono, rule setsum_strict_mono)
|
wenzelm@53255
|
987 |
fix i :: "'a"
|
wenzelm@53255
|
988 |
assume i: "i \<in> Basis"
|
wenzelm@53255
|
989 |
have "a i < y\<bullet>i \<and> y\<bullet>i < b i"
|
wenzelm@53255
|
990 |
using * i by (auto simp: box_def)
|
wenzelm@53255
|
991 |
moreover have "a i < x\<bullet>i" "x\<bullet>i - a i < e'"
|
wenzelm@53255
|
992 |
using a by auto
|
wenzelm@53255
|
993 |
moreover have "x\<bullet>i < b i" "b i - x\<bullet>i < e'"
|
wenzelm@53255
|
994 |
using b by auto
|
wenzelm@53255
|
995 |
ultimately have "\<bar>x\<bullet>i - y\<bullet>i\<bar> < 2 * e'"
|
wenzelm@53255
|
996 |
by auto
|
hoelzl@50526
|
997 |
then have "dist (x \<bullet> i) (y \<bullet> i) < e/sqrt (real (DIM('a)))"
|
immler@50087
|
998 |
unfolding e'_def by (auto simp: dist_real_def)
|
wenzelm@53015
|
999 |
then have "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < (e/sqrt (real (DIM('a))))\<^sup>2"
|
immler@50087
|
1000 |
by (rule power_strict_mono) auto
|
wenzelm@53015
|
1001 |
then show "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < e\<^sup>2 / real DIM('a)"
|
immler@50087
|
1002 |
by (simp add: power_divide)
|
immler@50087
|
1003 |
qed auto
|
wenzelm@53255
|
1004 |
also have "\<dots> = e"
|
lp15@61609
|
1005 |
using \<open>0 < e\<close> by simp
|
wenzelm@53255
|
1006 |
finally show "y \<in> ball x e"
|
wenzelm@53255
|
1007 |
by (auto simp: ball_def)
|
hoelzl@50526
|
1008 |
qed (insert a b, auto simp: box_def)
|
hoelzl@50526
|
1009 |
qed
|
immler@51103
|
1010 |
|
hoelzl@50526
|
1011 |
lemma open_UNION_box:
|
wenzelm@61076
|
1012 |
fixes M :: "'a::euclidean_space set"
|
wenzelm@53282
|
1013 |
assumes "open M"
|
hoelzl@50526
|
1014 |
defines "a' \<equiv> \<lambda>f :: 'a \<Rightarrow> real \<times> real. (\<Sum>(i::'a)\<in>Basis. fst (f i) *\<^sub>R i)"
|
hoelzl@50526
|
1015 |
defines "b' \<equiv> \<lambda>f :: 'a \<Rightarrow> real \<times> real. (\<Sum>(i::'a)\<in>Basis. snd (f i) *\<^sub>R i)"
|
wenzelm@53015
|
1016 |
defines "I \<equiv> {f\<in>Basis \<rightarrow>\<^sub>E \<rat> \<times> \<rat>. box (a' f) (b' f) \<subseteq> M}"
|
hoelzl@50526
|
1017 |
shows "M = (\<Union>f\<in>I. box (a' f) (b' f))"
|
wenzelm@52624
|
1018 |
proof -
|
wenzelm@60462
|
1019 |
have "x \<in> (\<Union>f\<in>I. box (a' f) (b' f))" if "x \<in> M" for x
|
wenzelm@60462
|
1020 |
proof -
|
wenzelm@52624
|
1021 |
obtain e where e: "e > 0" "ball x e \<subseteq> M"
|
wenzelm@60420
|
1022 |
using openE[OF \<open>open M\<close> \<open>x \<in> M\<close>] by auto
|
wenzelm@53282
|
1023 |
moreover obtain a b where ab:
|
wenzelm@53282
|
1024 |
"x \<in> box a b"
|
wenzelm@53282
|
1025 |
"\<forall>i \<in> Basis. a \<bullet> i \<in> \<rat>"
|
wenzelm@53282
|
1026 |
"\<forall>i\<in>Basis. b \<bullet> i \<in> \<rat>"
|
wenzelm@53282
|
1027 |
"box a b \<subseteq> ball x e"
|
wenzelm@52624
|
1028 |
using rational_boxes[OF e(1)] by metis
|
wenzelm@60462
|
1029 |
ultimately show ?thesis
|
wenzelm@52624
|
1030 |
by (intro UN_I[of "\<lambda>i\<in>Basis. (a \<bullet> i, b \<bullet> i)"])
|
wenzelm@52624
|
1031 |
(auto simp: euclidean_representation I_def a'_def b'_def)
|
wenzelm@60462
|
1032 |
qed
|
wenzelm@52624
|
1033 |
then show ?thesis by (auto simp: I_def)
|
wenzelm@52624
|
1034 |
qed
|
wenzelm@52624
|
1035 |
|
immler@56189
|
1036 |
lemma box_eq_empty:
|
immler@56189
|
1037 |
fixes a :: "'a::euclidean_space"
|
immler@56189
|
1038 |
shows "(box a b = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i))" (is ?th1)
|
immler@56189
|
1039 |
and "(cbox a b = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i < a\<bullet>i))" (is ?th2)
|
immler@56189
|
1040 |
proof -
|
immler@56189
|
1041 |
{
|
immler@56189
|
1042 |
fix i x
|
immler@56189
|
1043 |
assume i: "i\<in>Basis" and as:"b\<bullet>i \<le> a\<bullet>i" and x:"x\<in>box a b"
|
immler@56189
|
1044 |
then have "a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i"
|
immler@56189
|
1045 |
unfolding mem_box by (auto simp: box_def)
|
immler@56189
|
1046 |
then have "a\<bullet>i < b\<bullet>i" by auto
|
immler@56189
|
1047 |
then have False using as by auto
|
immler@56189
|
1048 |
}
|
immler@56189
|
1049 |
moreover
|
immler@56189
|
1050 |
{
|
immler@56189
|
1051 |
assume as: "\<forall>i\<in>Basis. \<not> (b\<bullet>i \<le> a\<bullet>i)"
|
immler@56189
|
1052 |
let ?x = "(1/2) *\<^sub>R (a + b)"
|
immler@56189
|
1053 |
{
|
immler@56189
|
1054 |
fix i :: 'a
|
immler@56189
|
1055 |
assume i: "i \<in> Basis"
|
immler@56189
|
1056 |
have "a\<bullet>i < b\<bullet>i"
|
immler@56189
|
1057 |
using as[THEN bspec[where x=i]] i by auto
|
immler@56189
|
1058 |
then have "a\<bullet>i < ((1/2) *\<^sub>R (a+b)) \<bullet> i" "((1/2) *\<^sub>R (a+b)) \<bullet> i < b\<bullet>i"
|
immler@56189
|
1059 |
by (auto simp: inner_add_left)
|
immler@56189
|
1060 |
}
|
immler@56189
|
1061 |
then have "box a b \<noteq> {}"
|
immler@56189
|
1062 |
using mem_box(1)[of "?x" a b] by auto
|
immler@56189
|
1063 |
}
|
immler@56189
|
1064 |
ultimately show ?th1 by blast
|
immler@56189
|
1065 |
|
immler@56189
|
1066 |
{
|
immler@56189
|
1067 |
fix i x
|
immler@56189
|
1068 |
assume i: "i \<in> Basis" and as:"b\<bullet>i < a\<bullet>i" and x:"x\<in>cbox a b"
|
immler@56189
|
1069 |
then have "a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i"
|
immler@56189
|
1070 |
unfolding mem_box by auto
|
immler@56189
|
1071 |
then have "a\<bullet>i \<le> b\<bullet>i" by auto
|
immler@56189
|
1072 |
then have False using as by auto
|
immler@56189
|
1073 |
}
|
immler@56189
|
1074 |
moreover
|
immler@56189
|
1075 |
{
|
immler@56189
|
1076 |
assume as:"\<forall>i\<in>Basis. \<not> (b\<bullet>i < a\<bullet>i)"
|
immler@56189
|
1077 |
let ?x = "(1/2) *\<^sub>R (a + b)"
|
immler@56189
|
1078 |
{
|
immler@56189
|
1079 |
fix i :: 'a
|
immler@56189
|
1080 |
assume i:"i \<in> Basis"
|
immler@56189
|
1081 |
have "a\<bullet>i \<le> b\<bullet>i"
|
immler@56189
|
1082 |
using as[THEN bspec[where x=i]] i by auto
|
immler@56189
|
1083 |
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"
|
immler@56189
|
1084 |
by (auto simp: inner_add_left)
|
immler@56189
|
1085 |
}
|
immler@56189
|
1086 |
then have "cbox a b \<noteq> {}"
|
immler@56189
|
1087 |
using mem_box(2)[of "?x" a b] by auto
|
immler@56189
|
1088 |
}
|
immler@56189
|
1089 |
ultimately show ?th2 by blast
|
immler@56189
|
1090 |
qed
|
immler@56189
|
1091 |
|
immler@56189
|
1092 |
lemma box_ne_empty:
|
immler@56189
|
1093 |
fixes a :: "'a::euclidean_space"
|
immler@56189
|
1094 |
shows "cbox a b \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i)"
|
immler@56189
|
1095 |
and "box a b \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
|
immler@56189
|
1096 |
unfolding box_eq_empty[of a b] by fastforce+
|
immler@56189
|
1097 |
|
immler@56189
|
1098 |
lemma
|
immler@56189
|
1099 |
fixes a :: "'a::euclidean_space"
|
immler@56189
|
1100 |
shows cbox_sing: "cbox a a = {a}"
|
immler@56189
|
1101 |
and box_sing: "box a a = {}"
|
immler@56189
|
1102 |
unfolding set_eq_iff mem_box eq_iff [symmetric]
|
immler@56189
|
1103 |
by (auto intro!: euclidean_eqI[where 'a='a])
|
immler@56189
|
1104 |
(metis all_not_in_conv nonempty_Basis)
|
immler@56189
|
1105 |
|
immler@56189
|
1106 |
lemma subset_box_imp:
|
immler@56189
|
1107 |
fixes a :: "'a::euclidean_space"
|
immler@56189
|
1108 |
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"
|
immler@56189
|
1109 |
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"
|
immler@56189
|
1110 |
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"
|
immler@56189
|
1111 |
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"
|
immler@56189
|
1112 |
unfolding subset_eq[unfolded Ball_def] unfolding mem_box
|
wenzelm@58757
|
1113 |
by (best intro: order_trans less_le_trans le_less_trans less_imp_le)+
|
immler@56189
|
1114 |
|
immler@56189
|
1115 |
lemma box_subset_cbox:
|
immler@56189
|
1116 |
fixes a :: "'a::euclidean_space"
|
immler@56189
|
1117 |
shows "box a b \<subseteq> cbox a b"
|
immler@56189
|
1118 |
unfolding subset_eq [unfolded Ball_def] mem_box
|
immler@56189
|
1119 |
by (fast intro: less_imp_le)
|
immler@56189
|
1120 |
|
immler@56189
|
1121 |
lemma subset_box:
|
immler@56189
|
1122 |
fixes a :: "'a::euclidean_space"
|
immler@56189
|
1123 |
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)
|
immler@56189
|
1124 |
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)
|
immler@56189
|
1125 |
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)
|
immler@56189
|
1126 |
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)
|
immler@56189
|
1127 |
proof -
|
immler@56189
|
1128 |
show ?th1
|
immler@56189
|
1129 |
unfolding subset_eq and Ball_def and mem_box
|
immler@56189
|
1130 |
by (auto intro: order_trans)
|
immler@56189
|
1131 |
show ?th2
|
immler@56189
|
1132 |
unfolding subset_eq and Ball_def and mem_box
|
immler@56189
|
1133 |
by (auto intro: le_less_trans less_le_trans order_trans less_imp_le)
|
immler@56189
|
1134 |
{
|
immler@56189
|
1135 |
assume as: "box c d \<subseteq> cbox a b" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
|
immler@56189
|
1136 |
then have "box c d \<noteq> {}"
|
immler@56189
|
1137 |
unfolding box_eq_empty by auto
|
immler@56189
|
1138 |
fix i :: 'a
|
immler@56189
|
1139 |
assume i: "i \<in> Basis"
|
immler@56189
|
1140 |
(** TODO combine the following two parts as done in the HOL_light version. **)
|
immler@56189
|
1141 |
{
|
immler@56189
|
1142 |
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"
|
immler@56189
|
1143 |
assume as2: "a\<bullet>i > c\<bullet>i"
|
immler@56189
|
1144 |
{
|
immler@56189
|
1145 |
fix j :: 'a
|
immler@56189
|
1146 |
assume j: "j \<in> Basis"
|
immler@56189
|
1147 |
then have "c \<bullet> j < ?x \<bullet> j \<and> ?x \<bullet> j < d \<bullet> j"
|
immler@56189
|
1148 |
apply (cases "j = i")
|
immler@56189
|
1149 |
using as(2)[THEN bspec[where x=j]] i
|
immler@56189
|
1150 |
apply (auto simp add: as2)
|
immler@56189
|
1151 |
done
|
immler@56189
|
1152 |
}
|
immler@56189
|
1153 |
then have "?x\<in>box c d"
|
immler@56189
|
1154 |
using i unfolding mem_box by auto
|
immler@56189
|
1155 |
moreover
|
immler@56189
|
1156 |
have "?x \<notin> cbox a b"
|
immler@56189
|
1157 |
unfolding mem_box
|
immler@56189
|
1158 |
apply auto
|
immler@56189
|
1159 |
apply (rule_tac x=i in bexI)
|
immler@56189
|
1160 |
using as(2)[THEN bspec[where x=i]] and as2 i
|
immler@56189
|
1161 |
apply auto
|
immler@56189
|
1162 |
done
|
immler@56189
|
1163 |
ultimately have False using as by auto
|
immler@56189
|
1164 |
}
|
immler@56189
|
1165 |
then have "a\<bullet>i \<le> c\<bullet>i" by (rule ccontr) auto
|
immler@56189
|
1166 |
moreover
|
immler@56189
|
1167 |
{
|
immler@56189
|
1168 |
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"
|
immler@56189
|
1169 |
assume as2: "b\<bullet>i < d\<bullet>i"
|
immler@56189
|
1170 |
{
|
immler@56189
|
1171 |
fix j :: 'a
|
immler@56189
|
1172 |
assume "j\<in>Basis"
|
immler@56189
|
1173 |
then have "d \<bullet> j > ?x \<bullet> j \<and> ?x \<bullet> j > c \<bullet> j"
|
immler@56189
|
1174 |
apply (cases "j = i")
|
immler@56189
|
1175 |
using as(2)[THEN bspec[where x=j]]
|
immler@56189
|
1176 |
apply (auto simp add: as2)
|
immler@56189
|
1177 |
done
|
immler@56189
|
1178 |
}
|
immler@56189
|
1179 |
then have "?x\<in>box c d"
|
immler@56189
|
1180 |
unfolding mem_box by auto
|
immler@56189
|
1181 |
moreover
|
immler@56189
|
1182 |
have "?x\<notin>cbox a b"
|
immler@56189
|
1183 |
unfolding mem_box
|
immler@56189
|
1184 |
apply auto
|
immler@56189
|
1185 |
apply (rule_tac x=i in bexI)
|
immler@56189
|
1186 |
using as(2)[THEN bspec[where x=i]] and as2 using i
|
immler@56189
|
1187 |
apply auto
|
immler@56189
|
1188 |
done
|
immler@56189
|
1189 |
ultimately have False using as by auto
|
immler@56189
|
1190 |
}
|
immler@56189
|
1191 |
then have "b\<bullet>i \<ge> d\<bullet>i" by (rule ccontr) auto
|
immler@56189
|
1192 |
ultimately
|
immler@56189
|
1193 |
have "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i" by auto
|
immler@56189
|
1194 |
} note part1 = this
|
immler@56189
|
1195 |
show ?th3
|
immler@56189
|
1196 |
unfolding subset_eq and Ball_def and mem_box
|
immler@56189
|
1197 |
apply (rule, rule, rule, rule)
|
immler@56189
|
1198 |
apply (rule part1)
|
immler@56189
|
1199 |
unfolding subset_eq and Ball_def and mem_box
|
immler@56189
|
1200 |
prefer 4
|
immler@56189
|
1201 |
apply auto
|
immler@56189
|
1202 |
apply (erule_tac x=xa in allE, erule_tac x=xa in allE, fastforce)+
|
immler@56189
|
1203 |
done
|
immler@56189
|
1204 |
{
|
immler@56189
|
1205 |
assume as: "box c d \<subseteq> box a b" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
|
immler@56189
|
1206 |
fix i :: 'a
|
immler@56189
|
1207 |
assume i:"i\<in>Basis"
|
immler@56189
|
1208 |
from as(1) have "box c d \<subseteq> cbox a b"
|
immler@56189
|
1209 |
using box_subset_cbox[of a b] by auto
|
immler@56189
|
1210 |
then have "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
|
immler@56189
|
1211 |
using part1 and as(2) using i by auto
|
immler@56189
|
1212 |
} note * = this
|
immler@56189
|
1213 |
show ?th4
|
immler@56189
|
1214 |
unfolding subset_eq and Ball_def and mem_box
|
immler@56189
|
1215 |
apply (rule, rule, rule, rule)
|
immler@56189
|
1216 |
apply (rule *)
|
immler@56189
|
1217 |
unfolding subset_eq and Ball_def and mem_box
|
immler@56189
|
1218 |
prefer 4
|
immler@56189
|
1219 |
apply auto
|
immler@56189
|
1220 |
apply (erule_tac x=xa in allE, simp)+
|
immler@56189
|
1221 |
done
|
immler@56189
|
1222 |
qed
|
immler@56189
|
1223 |
|
immler@56189
|
1224 |
lemma inter_interval:
|
immler@56189
|
1225 |
fixes a :: "'a::euclidean_space"
|
immler@56189
|
1226 |
shows "cbox a b \<inter> cbox c d =
|
immler@56189
|
1227 |
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)"
|
immler@56189
|
1228 |
unfolding set_eq_iff and Int_iff and mem_box
|
immler@56189
|
1229 |
by auto
|
immler@56189
|
1230 |
|
immler@56189
|
1231 |
lemma disjoint_interval:
|
immler@56189
|
1232 |
fixes a::"'a::euclidean_space"
|
immler@56189
|
1233 |
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)
|
immler@56189
|
1234 |
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)
|
immler@56189
|
1235 |
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)
|
immler@56189
|
1236 |
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)
|
immler@56189
|
1237 |
proof -
|
immler@56189
|
1238 |
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"
|
immler@56189
|
1239 |
have **: "\<And>P Q. (\<And>i :: 'a. i \<in> Basis \<Longrightarrow> Q ?z i \<Longrightarrow> P i) \<Longrightarrow>
|
immler@56189
|
1240 |
(\<And>i x :: 'a. i \<in> Basis \<Longrightarrow> P i \<Longrightarrow> Q x i) \<Longrightarrow> (\<forall>x. \<exists>i\<in>Basis. Q x i) \<longleftrightarrow> (\<exists>i\<in>Basis. P i)"
|
immler@56189
|
1241 |
by blast
|
immler@56189
|
1242 |
note * = set_eq_iff Int_iff empty_iff mem_box ball_conj_distrib[symmetric] eq_False ball_simps(10)
|
immler@56189
|
1243 |
show ?th1 unfolding * by (intro **) auto
|
immler@56189
|
1244 |
show ?th2 unfolding * by (intro **) auto
|
immler@56189
|
1245 |
show ?th3 unfolding * by (intro **) auto
|
immler@56189
|
1246 |
show ?th4 unfolding * by (intro **) auto
|
immler@56189
|
1247 |
qed
|
immler@56189
|
1248 |
|
hoelzl@57447
|
1249 |
lemma UN_box_eq_UNIV: "(\<Union>i::nat. box (- (real i *\<^sub>R One)) (real i *\<^sub>R One)) = UNIV"
|
hoelzl@57447
|
1250 |
proof -
|
lp15@61609
|
1251 |
have "\<bar>x \<bullet> b\<bar> < real_of_int (ceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)) + 1)"
|
wenzelm@60462
|
1252 |
if [simp]: "b \<in> Basis" for x b :: 'a
|
wenzelm@60462
|
1253 |
proof -
|
lp15@61609
|
1254 |
have "\<bar>x \<bullet> b\<bar> \<le> real_of_int (ceiling \<bar>x \<bullet> b\<bar>)"
|
lp15@61609
|
1255 |
by (rule le_of_int_ceiling)
|
lp15@61609
|
1256 |
also have "\<dots> \<le> real_of_int (ceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)))"
|
nipkow@59587
|
1257 |
by (auto intro!: ceiling_mono)
|
lp15@61609
|
1258 |
also have "\<dots> < real_of_int (ceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)) + 1)"
|
hoelzl@57447
|
1259 |
by simp
|
wenzelm@60462
|
1260 |
finally show ?thesis .
|
wenzelm@60462
|
1261 |
qed
|
wenzelm@60462
|
1262 |
then have "\<exists>n::nat. \<forall>b\<in>Basis. \<bar>x \<bullet> b\<bar> < real n" for x :: 'a
|
nipkow@59587
|
1263 |
by (metis order.strict_trans reals_Archimedean2)
|
hoelzl@57447
|
1264 |
moreover have "\<And>x b::'a. \<And>n::nat. \<bar>x \<bullet> b\<bar> < real n \<longleftrightarrow> - real n < x \<bullet> b \<and> x \<bullet> b < real n"
|
hoelzl@57447
|
1265 |
by auto
|
hoelzl@57447
|
1266 |
ultimately show ?thesis
|
hoelzl@57447
|
1267 |
by (auto simp: box_def inner_setsum_left inner_Basis setsum.If_cases)
|
hoelzl@57447
|
1268 |
qed
|
hoelzl@57447
|
1269 |
|
wenzelm@60420
|
1270 |
text \<open>Intervals in general, including infinite and mixtures of open and closed.\<close>
|
immler@56189
|
1271 |
|
immler@56189
|
1272 |
definition "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
|
immler@56189
|
1273 |
(\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i\<in>Basis. ((a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i) \<or> (b\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> a\<bullet>i))) \<longrightarrow> x \<in> s)"
|
immler@56189
|
1274 |
|
immler@56189
|
1275 |
lemma is_interval_cbox: "is_interval (cbox a (b::'a::euclidean_space))" (is ?th1)
|
immler@56189
|
1276 |
and is_interval_box: "is_interval (box a b)" (is ?th2)
|
immler@56189
|
1277 |
unfolding is_interval_def mem_box Ball_def atLeastAtMost_iff
|
immler@56189
|
1278 |
by (meson order_trans le_less_trans less_le_trans less_trans)+
|
immler@56189
|
1279 |
|
lp15@61609
|
1280 |
lemma is_interval_empty [iff]: "is_interval {}"
|
lp15@61609
|
1281 |
unfolding is_interval_def by simp
|
lp15@61609
|
1282 |
|
lp15@61609
|
1283 |
lemma is_interval_univ [iff]: "is_interval UNIV"
|
lp15@61609
|
1284 |
unfolding is_interval_def by simp
|
immler@56189
|
1285 |
|
immler@56189
|
1286 |
lemma mem_is_intervalI:
|
immler@56189
|
1287 |
assumes "is_interval s"
|
immler@56189
|
1288 |
assumes "a \<in> s" "b \<in> s"
|
immler@56189
|
1289 |
assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i \<or> b \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> a \<bullet> i"
|
immler@56189
|
1290 |
shows "x \<in> s"
|
immler@56189
|
1291 |
by (rule assms(1)[simplified is_interval_def, rule_format, OF assms(2,3,4)])
|
immler@56189
|
1292 |
|
immler@56189
|
1293 |
lemma interval_subst:
|
immler@56189
|
1294 |
fixes S::"'a::euclidean_space set"
|
immler@56189
|
1295 |
assumes "is_interval S"
|
immler@56189
|
1296 |
assumes "x \<in> S" "y j \<in> S"
|
immler@56189
|
1297 |
assumes "j \<in> Basis"
|
immler@56189
|
1298 |
shows "(\<Sum>i\<in>Basis. (if i = j then y i \<bullet> i else x \<bullet> i) *\<^sub>R i) \<in> S"
|
immler@56189
|
1299 |
by (rule mem_is_intervalI[OF assms(1,2)]) (auto simp: assms)
|
immler@56189
|
1300 |
|
immler@56189
|
1301 |
lemma mem_box_componentwiseI:
|
immler@56189
|
1302 |
fixes S::"'a::euclidean_space set"
|
immler@56189
|
1303 |
assumes "is_interval S"
|
immler@56189
|
1304 |
assumes "\<And>i. i \<in> Basis \<Longrightarrow> x \<bullet> i \<in> ((\<lambda>x. x \<bullet> i) ` S)"
|
immler@56189
|
1305 |
shows "x \<in> S"
|
immler@56189
|
1306 |
proof -
|
immler@56189
|
1307 |
from assms have "\<forall>i \<in> Basis. \<exists>s \<in> S. x \<bullet> i = s \<bullet> i"
|
immler@56189
|
1308 |
by auto
|
immler@56189
|
1309 |
with finite_Basis obtain s and bs::"'a list" where
|
immler@56189
|
1310 |
s: "\<And>i. i \<in> Basis \<Longrightarrow> x \<bullet> i = s i \<bullet> i" "\<And>i. i \<in> Basis \<Longrightarrow> s i \<in> S" and
|
immler@56189
|
1311 |
bs: "set bs = Basis" "distinct bs"
|
immler@56189
|
1312 |
by (metis finite_distinct_list)
|
immler@56189
|
1313 |
from nonempty_Basis s obtain j where j: "j \<in> Basis" "s j \<in> S" by blast
|
immler@56189
|
1314 |
def y \<equiv> "rec_list
|
immler@56189
|
1315 |
(s j)
|
immler@56189
|
1316 |
(\<lambda>j _ Y. (\<Sum>i\<in>Basis. (if i = j then s i \<bullet> i else Y \<bullet> i) *\<^sub>R i))"
|
immler@56189
|
1317 |
have "x = (\<Sum>i\<in>Basis. (if i \<in> set bs then s i \<bullet> i else s j \<bullet> i) *\<^sub>R i)"
|
immler@56189
|
1318 |
using bs by (auto simp add: s(1)[symmetric] euclidean_representation)
|
immler@56189
|
1319 |
also have [symmetric]: "y bs = \<dots>"
|
immler@56189
|
1320 |
using bs(2) bs(1)[THEN equalityD1]
|
immler@56189
|
1321 |
by (induct bs) (auto simp: y_def euclidean_representation intro!: euclidean_eqI[where 'a='a])
|
immler@56189
|
1322 |
also have "y bs \<in> S"
|
immler@56189
|
1323 |
using bs(1)[THEN equalityD1]
|
immler@56189
|
1324 |
apply (induct bs)
|
immler@56189
|
1325 |
apply (auto simp: y_def j)
|
immler@56189
|
1326 |
apply (rule interval_subst[OF assms(1)])
|
immler@56189
|
1327 |
apply (auto simp: s)
|
immler@56189
|
1328 |
done
|
immler@56189
|
1329 |
finally show ?thesis .
|
immler@56189
|
1330 |
qed
|
immler@56189
|
1331 |
|
himmelma@33175
|
1332 |
|
wenzelm@60420
|
1333 |
subsection\<open>Connectedness\<close>
|
himmelma@33175
|
1334 |
|
himmelma@33175
|
1335 |
lemma connected_local:
|
wenzelm@53255
|
1336 |
"connected S \<longleftrightarrow>
|
wenzelm@53255
|
1337 |
\<not> (\<exists>e1 e2.
|
wenzelm@53255
|
1338 |
openin (subtopology euclidean S) e1 \<and>
|
wenzelm@53255
|
1339 |
openin (subtopology euclidean S) e2 \<and>
|
wenzelm@53255
|
1340 |
S \<subseteq> e1 \<union> e2 \<and>
|
wenzelm@53255
|
1341 |
e1 \<inter> e2 = {} \<and>
|
wenzelm@53255
|
1342 |
e1 \<noteq> {} \<and>
|
wenzelm@53255
|
1343 |
e2 \<noteq> {})"
|
wenzelm@53282
|
1344 |
unfolding connected_def openin_open
|
lp15@59765
|
1345 |
by safe blast+
|
himmelma@33175
|
1346 |
|
huffman@34105
|
1347 |
lemma exists_diff:
|
huffman@34105
|
1348 |
fixes P :: "'a set \<Rightarrow> bool"
|
wenzelm@60462
|
1349 |
shows "(\<exists>S. P (- S)) \<longleftrightarrow> (\<exists>S. P S)" (is "?lhs \<longleftrightarrow> ?rhs")
|
wenzelm@53255
|
1350 |
proof -
|
wenzelm@53255
|
1351 |
{
|
wenzelm@53255
|
1352 |
assume "?lhs"
|
wenzelm@53255
|
1353 |
then have ?rhs by blast
|
wenzelm@53255
|
1354 |
}
|
himmelma@33175
|
1355 |
moreover
|
wenzelm@53255
|
1356 |
{
|
wenzelm@53255
|
1357 |
fix S
|
wenzelm@53255
|
1358 |
assume H: "P S"
|
huffman@34105
|
1359 |
have "S = - (- S)" by auto
|
wenzelm@53255
|
1360 |
with H have "P (- (- S))" by metis
|
wenzelm@53255
|
1361 |
}
|
himmelma@33175
|
1362 |
ultimately show ?thesis by metis
|
himmelma@33175
|
1363 |
qed
|
himmelma@33175
|
1364 |
|
himmelma@33175
|
1365 |
lemma connected_clopen: "connected S \<longleftrightarrow>
|
wenzelm@53255
|
1366 |
(\<forall>T. openin (subtopology euclidean S) T \<and>
|
wenzelm@53255
|
1367 |
closedin (subtopology euclidean S) T \<longrightarrow> T = {} \<or> T = S)" (is "?lhs \<longleftrightarrow> ?rhs")
|
wenzelm@53255
|
1368 |
proof -
|
wenzelm@53255
|
1369 |
have "\<not> connected S \<longleftrightarrow>
|
wenzelm@53255
|
1370 |
(\<exists>e1 e2. open e1 \<and> open (- e2) \<and> S \<subseteq> e1 \<union> (- e2) \<and> e1 \<inter> (- e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (- e2) \<inter> S \<noteq> {})"
|
himmelma@33175
|
1371 |
unfolding connected_def openin_open closedin_closed
|
lp15@55775
|
1372 |
by (metis double_complement)
|
wenzelm@53282
|
1373 |
then have th0: "connected S \<longleftrightarrow>
|
wenzelm@53255
|
1374 |
\<not> (\<exists>e2 e1. closed e2 \<and> open e1 \<and> S \<subseteq> e1 \<union> (- e2) \<and> e1 \<inter> (- e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (- e2) \<inter> S \<noteq> {})"
|
wenzelm@52624
|
1375 |
(is " _ \<longleftrightarrow> \<not> (\<exists>e2 e1. ?P e2 e1)")
|
wenzelm@52624
|
1376 |
apply (simp add: closed_def)
|
wenzelm@52624
|
1377 |
apply metis
|
wenzelm@52624
|
1378 |
done
|
himmelma@33175
|
1379 |
have th1: "?rhs \<longleftrightarrow> \<not> (\<exists>t' t. closed t'\<and>t = S\<inter>t' \<and> t\<noteq>{} \<and> t\<noteq>S \<and> (\<exists>t'. open t' \<and> t = S \<inter> t'))"
|
himmelma@33175
|
1380 |
(is "_ \<longleftrightarrow> \<not> (\<exists>t' t. ?Q t' t)")
|
himmelma@33175
|
1381 |
unfolding connected_def openin_open closedin_closed by auto
|
wenzelm@53255
|
1382 |
{
|
wenzelm@53255
|
1383 |
fix e2
|
wenzelm@53255
|
1384 |
{
|
wenzelm@53255
|
1385 |
fix e1
|
wenzelm@53282
|
1386 |
have "?P e2 e1 \<longleftrightarrow> (\<exists>t. closed e2 \<and> t = S\<inter>e2 \<and> open e1 \<and> t = S\<inter>e1 \<and> t\<noteq>{} \<and> t \<noteq> S)"
|
wenzelm@53255
|
1387 |
by auto
|
wenzelm@53255
|
1388 |
}
|
wenzelm@53255
|
1389 |
then have "(\<exists>e1. ?P e2 e1) \<longleftrightarrow> (\<exists>t. ?Q e2 t)"
|
wenzelm@53255
|
1390 |
by metis
|
wenzelm@53255
|
1391 |
}
|
wenzelm@53255
|
1392 |
then have "\<forall>e2. (\<exists>e1. ?P e2 e1) \<longleftrightarrow> (\<exists>t. ?Q e2 t)"
|
wenzelm@53255
|
1393 |
by blast
|
wenzelm@53255
|
1394 |
then show ?thesis
|
wenzelm@53255
|
1395 |
unfolding th0 th1 by simp
|
himmelma@33175
|
1396 |
qed
|
himmelma@33175
|
1397 |
|
wenzelm@60420
|
1398 |
subsection\<open>Limit points\<close>
|
himmelma@33175
|
1399 |
|
wenzelm@53282
|
1400 |
definition (in topological_space) islimpt:: "'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "islimpt" 60)
|
wenzelm@53255
|
1401 |
where "x islimpt S \<longleftrightarrow> (\<forall>T. x\<in>T \<longrightarrow> open T \<longrightarrow> (\<exists>y\<in>S. y\<in>T \<and> y\<noteq>x))"
|
himmelma@33175
|
1402 |
|
himmelma@33175
|
1403 |
lemma islimptI:
|
himmelma@33175
|
1404 |
assumes "\<And>T. x \<in> T \<Longrightarrow> open T \<Longrightarrow> \<exists>y\<in>S. y \<in> T \<and> y \<noteq> x"
|
himmelma@33175
|
1405 |
shows "x islimpt S"
|
himmelma@33175
|
1406 |
using assms unfolding islimpt_def by auto
|
himmelma@33175
|
1407 |
|
himmelma@33175
|
1408 |
lemma islimptE:
|
himmelma@33175
|
1409 |
assumes "x islimpt S" and "x \<in> T" and "open T"
|
himmelma@33175
|
1410 |
obtains y where "y \<in> S" and "y \<in> T" and "y \<noteq> x"
|
himmelma@33175
|
1411 |
using assms unfolding islimpt_def by auto
|
himmelma@33175
|
1412 |
|
huffman@44584
|
1413 |
lemma islimpt_iff_eventually: "x islimpt S \<longleftrightarrow> \<not> eventually (\<lambda>y. y \<notin> S) (at x)"
|
huffman@44584
|
1414 |
unfolding islimpt_def eventually_at_topological by auto
|
huffman@44584
|
1415 |
|
wenzelm@53255
|
1416 |
lemma islimpt_subset: "x islimpt S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> x islimpt T"
|
huffman@44584
|
1417 |
unfolding islimpt_def by fast
|
himmelma@33175
|
1418 |
|
himmelma@33175
|
1419 |
lemma islimpt_approachable:
|
himmelma@33175
|
1420 |
fixes x :: "'a::metric_space"
|
himmelma@33175
|
1421 |
shows "x islimpt S \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e)"
|
huffman@44584
|
1422 |
unfolding islimpt_iff_eventually eventually_at by fast
|
himmelma@33175
|
1423 |
|
himmelma@33175
|
1424 |
lemma islimpt_approachable_le:
|
himmelma@33175
|
1425 |
fixes x :: "'a::metric_space"
|
wenzelm@53640
|
1426 |
shows "x islimpt S \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in> S. x' \<noteq> x \<and> dist x' x \<le> e)"
|
himmelma@33175
|
1427 |
unfolding islimpt_approachable
|
huffman@44584
|
1428 |
using approachable_lt_le [where f="\<lambda>y. dist y x" and P="\<lambda>y. y \<notin> S \<or> y = x",
|
huffman@44584
|
1429 |
THEN arg_cong [where f=Not]]
|
huffman@44584
|
1430 |
by (simp add: Bex_def conj_commute conj_left_commute)
|
himmelma@33175
|
1431 |
|
huffman@44571
|
1432 |
lemma islimpt_UNIV_iff: "x islimpt UNIV \<longleftrightarrow> \<not> open {x}"
|
huffman@44571
|
1433 |
unfolding islimpt_def by (safe, fast, case_tac "T = {x}", fast, fast)
|
huffman@44571
|
1434 |
|
hoelzl@51351
|
1435 |
lemma islimpt_punctured: "x islimpt S = x islimpt (S-{x})"
|
hoelzl@51351
|
1436 |
unfolding islimpt_def by blast
|
hoelzl@51351
|
1437 |
|
wenzelm@60420
|
1438 |
text \<open>A perfect space has no isolated points.\<close>
|
huffman@44210
|
1439 |
|
huffman@44571
|
1440 |
lemma islimpt_UNIV [simp, intro]: "(x::'a::perfect_space) islimpt UNIV"
|
huffman@44571
|
1441 |
unfolding islimpt_UNIV_iff by (rule not_open_singleton)
|
himmelma@33175
|
1442 |
|
himmelma@33175
|
1443 |
lemma perfect_choose_dist:
|
huffman@44072
|
1444 |
fixes x :: "'a::{perfect_space, metric_space}"
|
himmelma@33175
|
1445 |
shows "0 < r \<Longrightarrow> \<exists>a. a \<noteq> x \<and> dist a x < r"
|
wenzelm@53255
|
1446 |
using islimpt_UNIV [of x]
|
wenzelm@53255
|
1447 |
by (simp add: islimpt_approachable)
|
himmelma@33175
|
1448 |
|
himmelma@33175
|
1449 |
lemma closed_limpt: "closed S \<longleftrightarrow> (\<forall>x. x islimpt S \<longrightarrow> x \<in> S)"
|
himmelma@33175
|
1450 |
unfolding closed_def
|
himmelma@33175
|
1451 |
apply (subst open_subopen)
|
huffman@34105
|
1452 |
apply (simp add: islimpt_def subset_eq)
|
wenzelm@52624
|
1453 |
apply (metis ComplE ComplI)
|
wenzelm@52624
|
1454 |
done
|
himmelma@33175
|
1455 |
|
himmelma@33175
|
1456 |
lemma islimpt_EMPTY[simp]: "\<not> x islimpt {}"
|
himmelma@33175
|
1457 |
unfolding islimpt_def by auto
|
himmelma@33175
|
1458 |
|
himmelma@33175
|
1459 |
lemma finite_set_avoid:
|
himmelma@33175
|
1460 |
fixes a :: "'a::metric_space"
|
wenzelm@53255
|
1461 |
assumes fS: "finite S"
|
wenzelm@53640
|
1462 |
shows "\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<longrightarrow> d \<le> dist a x"
|
wenzelm@53255
|
1463 |
proof (induct rule: finite_induct[OF fS])
|
wenzelm@53255
|
1464 |
case 1
|
wenzelm@53255
|
1465 |
then show ?case by (auto intro: zero_less_one)
|
himmelma@33175
|
1466 |
next
|
himmelma@33175
|
1467 |
case (2 x F)
|
wenzelm@60462
|
1468 |
from 2 obtain d where d: "d > 0" "\<forall>x\<in>F. x \<noteq> a \<longrightarrow> d \<le> dist a x"
|
wenzelm@53255
|
1469 |
by blast
|
wenzelm@53255
|
1470 |
show ?case
|
wenzelm@53255
|
1471 |
proof (cases "x = a")
|
wenzelm@53255
|
1472 |
case True
|
wenzelm@53255
|
1473 |
then show ?thesis using d by auto
|
wenzelm@53255
|
1474 |
next
|
wenzelm@53255
|
1475 |
case False
|
himmelma@33175
|
1476 |
let ?d = "min d (dist a x)"
|
wenzelm@53255
|
1477 |
have dp: "?d > 0"
|
wenzelm@53255
|
1478 |
using False d(1) using dist_nz by auto
|
wenzelm@60462
|
1479 |
from d have d': "\<forall>x\<in>F. x \<noteq> a \<longrightarrow> ?d \<le> dist a x"
|
wenzelm@53255
|
1480 |
by auto
|
wenzelm@53255
|
1481 |
with dp False show ?thesis
|
wenzelm@53255
|
1482 |
by (auto intro!: exI[where x="?d"])
|
wenzelm@53255
|
1483 |
qed
|
himmelma@33175
|
1484 |
qed
|
himmelma@33175
|
1485 |
|
himmelma@33175
|
1486 |
lemma islimpt_Un: "x islimpt (S \<union> T) \<longleftrightarrow> x islimpt S \<or> x islimpt T"
|
huffman@50897
|
1487 |
by (simp add: islimpt_iff_eventually eventually_conj_iff)
|
himmelma@33175
|
1488 |
|
himmelma@33175
|
1489 |
lemma discrete_imp_closed:
|
himmelma@33175
|
1490 |
fixes S :: "'a::metric_space set"
|
wenzelm@53255
|
1491 |
assumes e: "0 < e"
|
wenzelm@53255
|
1492 |
and d: "\<forall>x \<in> S. \<forall>y \<in> S. dist y x < e \<longrightarrow> y = x"
|
himmelma@33175
|
1493 |
shows "closed S"
|
wenzelm@53255
|
1494 |
proof -
|
wenzelm@53255
|
1495 |
{
|
wenzelm@53255
|
1496 |
fix x
|
wenzelm@53255
|
1497 |
assume C: "\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e"
|
himmelma@33175
|
1498 |
from e have e2: "e/2 > 0" by arith
|
wenzelm@53282
|
1499 |
from C[rule_format, OF e2] obtain y where y: "y \<in> S" "y \<noteq> x" "dist y x < e/2"
|
wenzelm@53255
|
1500 |
by blast
|
himmelma@33175
|
1501 |
let ?m = "min (e/2) (dist x y) "
|
wenzelm@53255
|
1502 |
from e2 y(2) have mp: "?m > 0"
|
wenzelm@53291
|
1503 |
by (simp add: dist_nz[symmetric])
|
wenzelm@53282
|
1504 |
from C[rule_format, OF mp] obtain z where z: "z \<in> S" "z \<noteq> x" "dist z x < ?m"
|
wenzelm@53255
|
1505 |
by blast
|
himmelma@33175
|
1506 |
have th: "dist z y < e" using z y
|
himmelma@33175
|
1507 |
by (intro dist_triangle_lt [where z=x], simp)
|
himmelma@33175
|
1508 |
from d[rule_format, OF y(1) z(1) th] y z
|
himmelma@33175
|
1509 |
have False by (auto simp add: dist_commute)}
|
wenzelm@53255
|
1510 |
then show ?thesis
|
wenzelm@53255
|
1511 |
by (metis islimpt_approachable closed_limpt [where 'a='a])
|
himmelma@33175
|
1512 |
qed
|
himmelma@33175
|
1513 |
|
eberlm@61524
|
1514 |
lemma closed_of_nat_image: "closed (of_nat ` A :: 'a :: real_normed_algebra_1 set)"
|
eberlm@61524
|
1515 |
by (rule discrete_imp_closed[of 1]) (auto simp: dist_of_nat)
|
eberlm@61524
|
1516 |
|
eberlm@61524
|
1517 |
lemma closed_of_int_image: "closed (of_int ` A :: 'a :: real_normed_algebra_1 set)"
|
eberlm@61524
|
1518 |
by (rule discrete_imp_closed[of 1]) (auto simp: dist_of_int)
|
eberlm@61524
|
1519 |
|
eberlm@61524
|
1520 |
lemma closed_Nats [simp]: "closed (\<nat> :: 'a :: real_normed_algebra_1 set)"
|
eberlm@61524
|
1521 |
unfolding Nats_def by (rule closed_of_nat_image)
|
eberlm@61524
|
1522 |
|
eberlm@61524
|
1523 |
lemma closed_Ints [simp]: "closed (\<int> :: 'a :: real_normed_algebra_1 set)"
|
eberlm@61524
|
1524 |
unfolding Ints_def by (rule closed_of_int_image)
|
eberlm@61524
|
1525 |
|
huffman@44210
|
1526 |
|
wenzelm@60420
|
1527 |
subsection \<open>Interior of a Set\<close>
|
huffman@44210
|
1528 |
|
huffman@44519
|
1529 |
definition "interior S = \<Union>{T. open T \<and> T \<subseteq> S}"
|
huffman@44519
|
1530 |
|
huffman@44519
|
1531 |
lemma interiorI [intro?]:
|
huffman@44519
|
1532 |
assumes "open T" and "x \<in> T" and "T \<subseteq> S"
|
huffman@44519
|
1533 |
shows "x \<in> interior S"
|
huffman@44519
|
1534 |
using assms unfolding interior_def by fast
|
huffman@44519
|
1535 |
|
huffman@44519
|
1536 |
lemma interiorE [elim?]:
|
huffman@44519
|
1537 |
assumes "x \<in> interior S"
|
huffman@44519
|
1538 |
obtains T where "open T" and "x \<in> T" and "T \<subseteq> S"
|
huffman@44519
|
1539 |
using assms unfolding interior_def by fast
|
huffman@44519
|
1540 |
|
huffman@44519
|
1541 |
lemma open_interior [simp, intro]: "open (interior S)"
|
huffman@44519
|
1542 |
by (simp add: interior_def open_Union)
|
huffman@44519
|
1543 |
|
huffman@44519
|
1544 |
lemma interior_subset: "interior S \<subseteq> S"
|
huffman@44519
|
1545 |
by (auto simp add: interior_def)
|
huffman@44519
|
1546 |
|
huffman@44519
|
1547 |
lemma interior_maximal: "T \<subseteq> S \<Longrightarrow> open T \<Longrightarrow> T \<subseteq> interior S"
|
huffman@44519
|
1548 |
by (auto simp add: interior_def)
|
huffman@44519
|
1549 |
|
huffman@44519
|
1550 |
lemma interior_open: "open S \<Longrightarrow> interior S = S"
|
huffman@44519
|
1551 |
by (intro equalityI interior_subset interior_maximal subset_refl)
|
himmelma@33175
|
1552 |
|
himmelma@33175
|
1553 |
lemma interior_eq: "interior S = S \<longleftrightarrow> open S"
|
huffman@44519
|
1554 |
by (metis open_interior interior_open)
|
huffman@44519
|
1555 |
|
huffman@44519
|
1556 |
lemma open_subset_interior: "open S \<Longrightarrow> S \<subseteq> interior T \<longleftrightarrow> S \<subseteq> T"
|
himmelma@33175
|
1557 |
by (metis interior_maximal interior_subset subset_trans)
|
himmelma@33175
|
1558 |
|
huffman@44519
|
1559 |
lemma interior_empty [simp]: "interior {} = {}"
|
huffman@44519
|
1560 |
using open_empty by (rule interior_open)
|
huffman@44519
|
1561 |
|
huffman@44522
|
1562 |
lemma interior_UNIV [simp]: "interior UNIV = UNIV"
|
huffman@44522
|
1563 |
using open_UNIV by (rule interior_open)
|
huffman@44522
|
1564 |
|
huffman@44519
|
1565 |
lemma interior_interior [simp]: "interior (interior S) = interior S"
|
huffman@44519
|
1566 |
using open_interior by (rule interior_open)
|
huffman@44519
|
1567 |
|
huffman@44522
|
1568 |
lemma interior_mono: "S \<subseteq> T \<Longrightarrow> interior S \<subseteq> interior T"
|
huffman@44522
|
1569 |
by (auto simp add: interior_def)
|
huffman@44519
|
1570 |
|
huffman@44519
|
1571 |
lemma interior_unique:
|
huffman@44519
|
1572 |
assumes "T \<subseteq> S" and "open T"
|
huffman@44519
|
1573 |
assumes "\<And>T'. T' \<subseteq> S \<Longrightarrow> open T' \<Longrightarrow> T' \<subseteq> T"
|
huffman@44519
|
1574 |
shows "interior S = T"
|
huffman@44519
|
1575 |
by (intro equalityI assms interior_subset open_interior interior_maximal)
|
huffman@44519
|
1576 |
|
paulson@61518
|
1577 |
lemma interior_singleton [simp]:
|
paulson@61518
|
1578 |
fixes a :: "'a::perfect_space" shows "interior {a} = {}"
|
paulson@61518
|
1579 |
apply (rule interior_unique, simp_all)
|
paulson@61518
|
1580 |
using not_open_singleton subset_singletonD by fastforce
|
paulson@61518
|
1581 |
|
paulson@61518
|
1582 |
lemma interior_Int [simp]: "interior (S \<inter> T) = interior S \<inter> interior T"
|
huffman@44522
|
1583 |
by (intro equalityI Int_mono Int_greatest interior_mono Int_lower1
|
huffman@44519
|
1584 |
Int_lower2 interior_maximal interior_subset open_Int open_interior)
|
huffman@44519
|
1585 |
|
huffman@44519
|
1586 |
lemma mem_interior: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. ball x e \<subseteq> S)"
|
huffman@44519
|
1587 |
using open_contains_ball_eq [where S="interior S"]
|
huffman@44519
|
1588 |
by (simp add: open_subset_interior)
|
himmelma@33175
|
1589 |
|
eberlm@61531
|
1590 |
lemma eventually_nhds_in_nhd: "x \<in> interior s \<Longrightarrow> eventually (\<lambda>y. y \<in> s) (nhds x)"
|
eberlm@61531
|
1591 |
using interior_subset[of s] by (subst eventually_nhds) blast
|
eberlm@61531
|
1592 |
|
himmelma@33175
|
1593 |
lemma interior_limit_point [intro]:
|
himmelma@33175
|
1594 |
fixes x :: "'a::perfect_space"
|
wenzelm@53255
|
1595 |
assumes x: "x \<in> interior S"
|
wenzelm@53255
|
1596 |
shows "x islimpt S"
|
huffman@44072
|
1597 |
using x islimpt_UNIV [of x]
|
huffman@44072
|
1598 |
unfolding interior_def islimpt_def
|
huffman@44072
|
1599 |
apply (clarsimp, rename_tac T T')
|
huffman@44072
|
1600 |
apply (drule_tac x="T \<inter> T'" in spec)
|
huffman@44072
|
1601 |
apply (auto simp add: open_Int)
|
huffman@44072
|
1602 |
done
|
himmelma@33175
|
1603 |
|
himmelma@33175
|
1604 |
lemma interior_closed_Un_empty_interior:
|
wenzelm@53255
|
1605 |
assumes cS: "closed S"
|
wenzelm@53255
|
1606 |
and iT: "interior T = {}"
|
huffman@44519
|
1607 |
shows "interior (S \<union> T) = interior S"
|
himmelma@33175
|
1608 |
proof
|
huffman@44519
|
1609 |
show "interior S \<subseteq> interior (S \<union> T)"
|
wenzelm@53255
|
1610 |
by (rule interior_mono) (rule Un_upper1)
|
himmelma@33175
|
1611 |
show "interior (S \<union> T) \<subseteq> interior S"
|
himmelma@33175
|
1612 |
proof
|
wenzelm@53255
|
1613 |
fix x
|
wenzelm@53255
|
1614 |
assume "x \<in> interior (S \<union> T)"
|
huffman@44519
|
1615 |
then obtain R where "open R" "x \<in> R" "R \<subseteq> S \<union> T" ..
|
himmelma@33175
|
1616 |
show "x \<in> interior S"
|
himmelma@33175
|
1617 |
proof (rule ccontr)
|
himmelma@33175
|
1618 |
assume "x \<notin> interior S"
|
wenzelm@60420
|
1619 |
with \<open>x \<in> R\<close> \<open>open R\<close> obtain y where "y \<in> R - S"
|
huffman@44519
|
1620 |
unfolding interior_def by fast
|
wenzelm@60420
|
1621 |
from \<open>open R\<close> \<open>closed S\<close> have "open (R - S)"
|
wenzelm@53282
|
1622 |
by (rule open_Diff)
|
wenzelm@60420
|
1623 |
from \<open>R \<subseteq> S \<union> T\<close> have "R - S \<subseteq> T"
|
wenzelm@53282
|
1624 |
by fast
|
wenzelm@60420
|
1625 |
from \<open>y \<in> R - S\<close> \<open>open (R - S)\<close> \<open>R - S \<subseteq> T\<close> \<open>interior T = {}\<close> show False
|
wenzelm@53282
|
1626 |
unfolding interior_def by fast
|
himmelma@33175
|
1627 |
qed
|
himmelma@33175
|
1628 |
qed
|
himmelma@33175
|
1629 |
qed
|
himmelma@33175
|
1630 |
|
huffman@44365
|
1631 |
lemma interior_Times: "interior (A \<times> B) = interior A \<times> interior B"
|
huffman@44365
|
1632 |
proof (rule interior_unique)
|
huffman@44365
|
1633 |
show "interior A \<times> interior B \<subseteq> A \<times> B"
|
huffman@44365
|
1634 |
by (intro Sigma_mono interior_subset)
|
huffman@44365
|
1635 |
show "open (interior A \<times> interior B)"
|
huffman@44365
|
1636 |
by (intro open_Times open_interior)
|
wenzelm@53255
|
1637 |
fix T
|
wenzelm@53255
|
1638 |
assume "T \<subseteq> A \<times> B" and "open T"
|
wenzelm@53255
|
1639 |
then show "T \<subseteq> interior A \<times> interior B"
|
wenzelm@53282
|
1640 |
proof safe
|
wenzelm@53255
|
1641 |
fix x y
|
wenzelm@53255
|
1642 |
assume "(x, y) \<in> T"
|
huffman@44519
|
1643 |
then obtain C D where "open C" "open D" "C \<times> D \<subseteq> T" "x \<in> C" "y \<in> D"
|
wenzelm@60420
|
1644 |
using \<open>open T\<close> unfolding open_prod_def by fast
|
wenzelm@53255
|
1645 |
then have "open C" "open D" "C \<subseteq> A" "D \<subseteq> B" "x \<in> C" "y \<in> D"
|
wenzelm@60420
|
1646 |
using \<open>T \<subseteq> A \<times> B\<close> by auto
|
wenzelm@53255
|
1647 |
then show "x \<in> interior A" and "y \<in> interior B"
|
huffman@44519
|
1648 |
by (auto intro: interiorI)
|
huffman@44519
|
1649 |
qed
|
huffman@44365
|
1650 |
qed
|
huffman@44365
|
1651 |
|
hoelzl@61245
|
1652 |
lemma interior_Ici:
|
hoelzl@61245
|
1653 |
fixes x :: "'a :: {dense_linorder, linorder_topology}"
|
hoelzl@61245
|
1654 |
assumes "b < x"
|
hoelzl@61245
|
1655 |
shows "interior { x ..} = { x <..}"
|
hoelzl@61245
|
1656 |
proof (rule interior_unique)
|
hoelzl@61245
|
1657 |
fix T assume "T \<subseteq> {x ..}" "open T"
|
hoelzl@61245
|
1658 |
moreover have "x \<notin> T"
|
hoelzl@61245
|
1659 |
proof
|
hoelzl@61245
|
1660 |
assume "x \<in> T"
|
hoelzl@61245
|
1661 |
obtain y where "y < x" "{y <.. x} \<subseteq> T"
|
hoelzl@61245
|
1662 |
using open_left[OF \<open>open T\<close> \<open>x \<in> T\<close> \<open>b < x\<close>] by auto
|
hoelzl@61245
|
1663 |
with dense[OF \<open>y < x\<close>] obtain z where "z \<in> T" "z < x"
|
hoelzl@61245
|
1664 |
by (auto simp: subset_eq Ball_def)
|
hoelzl@61245
|
1665 |
with \<open>T \<subseteq> {x ..}\<close> show False by auto
|
hoelzl@61245
|
1666 |
qed
|
hoelzl@61245
|
1667 |
ultimately show "T \<subseteq> {x <..}"
|
hoelzl@61245
|
1668 |
by (auto simp: subset_eq less_le)
|
hoelzl@61245
|
1669 |
qed auto
|
hoelzl@61245
|
1670 |
|
hoelzl@61245
|
1671 |
lemma interior_Iic:
|
hoelzl@61245
|
1672 |
fixes x :: "'a :: {dense_linorder, linorder_topology}"
|
hoelzl@61245
|
1673 |
assumes "x < b"
|
hoelzl@61245
|
1674 |
shows "interior {.. x} = {..< x}"
|
hoelzl@61245
|
1675 |
proof (rule interior_unique)
|
hoelzl@61245
|
1676 |
fix T assume "T \<subseteq> {.. x}" "open T"
|
hoelzl@61245
|
1677 |
moreover have "x \<notin> T"
|
hoelzl@61245
|
1678 |
proof
|
hoelzl@61245
|
1679 |
assume "x \<in> T"
|
hoelzl@61245
|
1680 |
obtain y where "x < y" "{x ..< y} \<subseteq> T"
|
hoelzl@61245
|
1681 |
using open_right[OF \<open>open T\<close> \<open>x \<in> T\<close> \<open>x < b\<close>] by auto
|
hoelzl@61245
|
1682 |
with dense[OF \<open>x < y\<close>] obtain z where "z \<in> T" "x < z"
|
hoelzl@61245
|
1683 |
by (auto simp: subset_eq Ball_def less_le)
|
hoelzl@61245
|
1684 |
with \<open>T \<subseteq> {.. x}\<close> show False by auto
|
hoelzl@61245
|
1685 |
qed
|
hoelzl@61245
|
1686 |
ultimately show "T \<subseteq> {..< x}"
|
hoelzl@61245
|
1687 |
by (auto simp: subset_eq less_le)
|
hoelzl@61245
|
1688 |
qed auto
|
himmelma@33175
|
1689 |
|
wenzelm@60420
|
1690 |
subsection \<open>Closure of a Set\<close>
|
himmelma@33175
|
1691 |
|
himmelma@33175
|
1692 |
definition "closure S = S \<union> {x | x. x islimpt S}"
|
himmelma@33175
|
1693 |
|
huffman@44518
|
1694 |
lemma interior_closure: "interior S = - (closure (- S))"
|
huffman@44518
|
1695 |
unfolding interior_def closure_def islimpt_def by auto
|
huffman@44518
|
1696 |
|
huffman@34105
|
1697 |
lemma closure_interior: "closure S = - interior (- S)"
|
huffman@44518
|
1698 |
unfolding interior_closure by simp
|
himmelma@33175
|
1699 |
|
himmelma@33175
|
1700 |
lemma closed_closure[simp, intro]: "closed (closure S)"
|
huffman@44518
|
1701 |
unfolding closure_interior by (simp add: closed_Compl)
|
huffman@44518
|
1702 |
|
huffman@44518
|
1703 |
lemma closure_subset: "S \<subseteq> closure S"
|
huffman@44518
|
1704 |
unfolding closure_def by simp
|
himmelma@33175
|
1705 |
|
himmelma@33175
|
1706 |
lemma closure_hull: "closure S = closed hull S"
|
huffman@44519
|
1707 |
unfolding hull_def closure_interior interior_def by auto
|
himmelma@33175
|
1708 |
|
himmelma@33175
|
1709 |
lemma closure_eq: "closure S = S \<longleftrightarrow> closed S"
|
huffman@44519
|
1710 |
unfolding closure_hull using closed_Inter by (rule hull_eq)
|
huffman@44519
|
1711 |
|
huffman@44519
|
1712 |
lemma closure_closed [simp]: "closed S \<Longrightarrow> closure S = S"
|
huffman@44519
|
1713 |
unfolding closure_eq .
|
huffman@44519
|
1714 |
|
huffman@44519
|
1715 |
lemma closure_closure [simp]: "closure (closure S) = closure S"
|
huffman@44518
|
1716 |
unfolding closure_hull by (rule hull_hull)
|
himmelma@33175
|
1717 |
|
huffman@44522
|
1718 |
lemma closure_mono: "S \<subseteq> T \<Longrightarrow> closure S \<subseteq> closure T"
|
huffman@44518
|
1719 |
unfolding closure_hull by (rule hull_mono)
|
himmelma@33175
|
1720 |
|
huffman@44519
|
1721 |
lemma closure_minimal: "S \<subseteq> T \<Longrightarrow> closed T \<Longrightarrow> closure S \<subseteq> T"
|
huffman@44518
|
1722 |
unfolding closure_hull by (rule hull_minimal)
|
himmelma@33175
|
1723 |
|
huffman@44519
|
1724 |
lemma closure_unique:
|
wenzelm@53255
|
1725 |
assumes "S \<subseteq> T"
|
wenzelm@53255
|
1726 |
and "closed T"
|
wenzelm@53255
|
1727 |
and "\<And>T'. S \<subseteq> T' \<Longrightarrow> closed T' \<Longrightarrow> T \<subseteq> T'"
|
huffman@44519
|
1728 |
shows "closure S = T"
|
huffman@44519
|
1729 |
using assms unfolding closure_hull by (rule hull_unique)
|
huffman@44519
|
1730 |
|
huffman@44519
|
1731 |
lemma closure_empty [simp]: "closure {} = {}"
|
huffman@44518
|
1732 |
using closed_empty by (rule closure_closed)
|
himmelma@33175
|
1733 |
|
huffman@44522
|
1734 |
lemma closure_UNIV [simp]: "closure UNIV = UNIV"
|
huffman@44518
|
1735 |
using closed_UNIV by (rule closure_closed)
|
huffman@44518
|
1736 |
|
huffman@44518
|
1737 |
lemma closure_union [simp]: "closure (S \<union> T) = closure S \<union> closure T"
|
huffman@44518
|
1738 |
unfolding closure_interior by simp
|
himmelma@33175
|
1739 |
|
lp15@60974
|
1740 |
lemma closure_eq_empty [iff]: "closure S = {} \<longleftrightarrow> S = {}"
|
himmelma@33175
|
1741 |
using closure_empty closure_subset[of S]
|
himmelma@33175
|
1742 |
by blast
|
himmelma@33175
|
1743 |
|
himmelma@33175
|
1744 |
lemma closure_subset_eq: "closure S \<subseteq> S \<longleftrightarrow> closed S"
|
himmelma@33175
|
1745 |
using closure_eq[of S] closure_subset[of S]
|
himmelma@33175
|
1746 |
by simp
|
himmelma@33175
|
1747 |
|
himmelma@33175
|
1748 |
lemma open_inter_closure_eq_empty:
|
himmelma@33175
|
1749 |
"open S \<Longrightarrow> (S \<inter> closure T) = {} \<longleftrightarrow> S \<inter> T = {}"
|
huffman@34105
|
1750 |
using open_subset_interior[of S "- T"]
|
huffman@34105
|
1751 |
using interior_subset[of "- T"]
|
himmelma@33175
|
1752 |
unfolding closure_interior
|
himmelma@33175
|
1753 |
by auto
|
himmelma@33175
|
1754 |
|
himmelma@33175
|
1755 |
lemma open_inter_closure_subset:
|
himmelma@33175
|
1756 |
"open S \<Longrightarrow> (S \<inter> (closure T)) \<subseteq> closure(S \<inter> T)"
|
himmelma@33175
|
1757 |
proof
|
himmelma@33175
|
1758 |
fix x
|
himmelma@33175
|
1759 |
assume as: "open S" "x \<in> S \<inter> closure T"
|
wenzelm@53255
|
1760 |
{
|
wenzelm@53282
|
1761 |
assume *: "x islimpt T"
|
himmelma@33175
|
1762 |
have "x islimpt (S \<inter> T)"
|
himmelma@33175
|
1763 |
proof (rule islimptI)
|
himmelma@33175
|
1764 |
fix A
|
himmelma@33175
|
1765 |
assume "x \<in> A" "open A"
|
himmelma@33175
|
1766 |
with as have "x \<in> A \<inter> S" "open (A \<inter> S)"
|
himmelma@33175
|
1767 |
by (simp_all add: open_Int)
|
himmelma@33175
|
1768 |
with * obtain y where "y \<in> T" "y \<in> A \<inter> S" "y \<noteq> x"
|
himmelma@33175
|
1769 |
by (rule islimptE)
|
wenzelm@53255
|
1770 |
then have "y \<in> S \<inter> T" "y \<in> A \<and> y \<noteq> x"
|
himmelma@33175
|
1771 |
by simp_all
|
wenzelm@53255
|
1772 |
then show "\<exists>y\<in>(S \<inter> T). y \<in> A \<and> y \<noteq> x" ..
|
himmelma@33175
|
1773 |
qed
|
himmelma@33175
|
1774 |
}
|
himmelma@33175
|
1775 |
then show "x \<in> closure (S \<inter> T)" using as
|
himmelma@33175
|
1776 |
unfolding closure_def
|
himmelma@33175
|
1777 |
by blast
|
himmelma@33175
|
1778 |
qed
|
himmelma@33175
|
1779 |
|
huffman@44519
|
1780 |
lemma closure_complement: "closure (- S) = - interior S"
|
huffman@44518
|
1781 |
unfolding closure_interior by simp
|
himmelma@33175
|
1782 |
|
huffman@44519
|
1783 |
lemma interior_complement: "interior (- S) = - closure S"
|
huffman@44518
|
1784 |
unfolding closure_interior by simp
|
himmelma@33175
|
1785 |
|
huffman@44365
|
1786 |
lemma closure_Times: "closure (A \<times> B) = closure A \<times> closure B"
|
huffman@44519
|
1787 |
proof (rule closure_unique)
|
huffman@44365
|
1788 |
show "A \<times> B \<subseteq> closure A \<times> closure B"
|
huffman@44365
|
1789 |
by (intro Sigma_mono closure_subset)
|
huffman@44365
|
1790 |
show "closed (closure A \<times> closure B)"
|
huffman@44365
|
1791 |
by (intro closed_Times closed_closure)
|
wenzelm@53282
|
1792 |
fix T
|
wenzelm@53282
|
1793 |
assume "A \<times> B \<subseteq> T" and "closed T"
|
wenzelm@53282
|
1794 |
then show "closure A \<times> closure B \<subseteq> T"
|
huffman@44365
|
1795 |
apply (simp add: closed_def open_prod_def, clarify)
|
huffman@44365
|
1796 |
apply (rule ccontr)
|
huffman@44365
|
1797 |
apply (drule_tac x="(a, b)" in bspec, simp, clarify, rename_tac C D)
|
huffman@44365
|
1798 |
apply (simp add: closure_interior interior_def)
|
huffman@44365
|
1799 |
apply (drule_tac x=C in spec)
|
huffman@44365
|
1800 |
apply (drule_tac x=D in spec)
|
huffman@44365
|
1801 |
apply auto
|
huffman@44365
|
1802 |
done
|
huffman@44365
|
1803 |
qed
|
huffman@44365
|
1804 |
|
hoelzl@51351
|
1805 |
lemma islimpt_in_closure: "(x islimpt S) = (x:closure(S-{x}))"
|
hoelzl@51351
|
1806 |
unfolding closure_def using islimpt_punctured by blast
|
hoelzl@51351
|
1807 |
|
lp15@61306
|
1808 |
lemma connected_imp_connected_closure: "connected s \<Longrightarrow> connected (closure s)"
|
lp15@61306
|
1809 |
by (rule connectedI) (meson closure_subset open_Int open_inter_closure_eq_empty subset_trans connectedD)
|
lp15@61306
|
1810 |
|
lp15@61306
|
1811 |
lemma limpt_of_limpts:
|
lp15@61306
|
1812 |
fixes x :: "'a::metric_space"
|
lp15@61306
|
1813 |
shows "x islimpt {y. y islimpt s} \<Longrightarrow> x islimpt s"
|
lp15@61306
|
1814 |
apply (clarsimp simp add: islimpt_approachable)
|
lp15@61306
|
1815 |
apply (drule_tac x="e/2" in spec)
|
lp15@61306
|
1816 |
apply (auto simp: simp del: less_divide_eq_numeral1)
|
lp15@61306
|
1817 |
apply (drule_tac x="dist x' x" in spec)
|
lp15@61306
|
1818 |
apply (auto simp: zero_less_dist_iff simp del: less_divide_eq_numeral1)
|
lp15@61306
|
1819 |
apply (erule rev_bexI)
|
lp15@61306
|
1820 |
by (metis dist_commute dist_triangle_half_r less_trans less_irrefl)
|
lp15@61306
|
1821 |
|
lp15@61306
|
1822 |
lemma closed_limpts: "closed {x::'a::metric_space. x islimpt s}"
|
lp15@61306
|
1823 |
using closed_limpt limpt_of_limpts by blast
|
lp15@61306
|
1824 |
|
lp15@61306
|
1825 |
lemma limpt_of_closure:
|
lp15@61306
|
1826 |
fixes x :: "'a::metric_space"
|
lp15@61306
|
1827 |
shows "x islimpt closure s \<longleftrightarrow> x islimpt s"
|
lp15@61306
|
1828 |
by (auto simp: closure_def islimpt_Un dest: limpt_of_limpts)
|
lp15@61306
|
1829 |
|
lp15@61306
|
1830 |
lemma closed_in_limpt:
|
lp15@61306
|
1831 |
"closedin (subtopology euclidean t) s \<longleftrightarrow> s \<subseteq> t \<and> (\<forall>x. x islimpt s \<and> x \<in> t \<longrightarrow> x \<in> s)"
|
lp15@61306
|
1832 |
apply (simp add: closedin_closed, safe)
|
lp15@61306
|
1833 |
apply (simp add: closed_limpt islimpt_subset)
|
lp15@61306
|
1834 |
apply (rule_tac x="closure s" in exI)
|
lp15@61306
|
1835 |
apply simp
|
lp15@61306
|
1836 |
apply (force simp: closure_def)
|
lp15@61306
|
1837 |
done
|
lp15@61306
|
1838 |
|
paulson@61518
|
1839 |
lemma closedin_closed_eq:
|
paulson@61518
|
1840 |
"closed s \<Longrightarrow> (closedin (subtopology euclidean s) t \<longleftrightarrow> closed t \<and> t \<subseteq> s)"
|
paulson@61518
|
1841 |
by (meson closed_in_limpt closed_subset closedin_closed_trans)
|
paulson@61518
|
1842 |
|
eberlm@61531
|
1843 |
|
lp15@61306
|
1844 |
subsection\<open>Connected components, considered as a connectedness relation or a set\<close>
|
lp15@61306
|
1845 |
|
lp15@61306
|
1846 |
definition
|
lp15@61306
|
1847 |
"connected_component s x y \<equiv> \<exists>t. connected t \<and> t \<subseteq> s \<and> x \<in> t \<and> y \<in> t"
|
lp15@61306
|
1848 |
|
lp15@61306
|
1849 |
abbreviation
|
lp15@61306
|
1850 |
"connected_component_set s x \<equiv> Collect (connected_component s x)"
|
lp15@61306
|
1851 |
|
lp15@61426
|
1852 |
lemma connected_componentI:
|
lp15@61426
|
1853 |
"\<lbrakk>connected t; t \<subseteq> s; x \<in> t; y \<in> t\<rbrakk> \<Longrightarrow> connected_component s x y"
|
lp15@61426
|
1854 |
by (auto simp: connected_component_def)
|
lp15@61426
|
1855 |
|
lp15@61306
|
1856 |
lemma connected_component_in: "connected_component s x y \<Longrightarrow> x \<in> s \<and> y \<in> s"
|
lp15@61306
|
1857 |
by (auto simp: connected_component_def)
|
lp15@61306
|
1858 |
|
lp15@61306
|
1859 |
lemma connected_component_refl: "x \<in> s \<Longrightarrow> connected_component s x x"
|
lp15@61306
|
1860 |
apply (auto simp: connected_component_def)
|
lp15@61306
|
1861 |
using connected_sing by blast
|
lp15@61306
|
1862 |
|
lp15@61306
|
1863 |
lemma connected_component_refl_eq [simp]: "connected_component s x x \<longleftrightarrow> x \<in> s"
|
lp15@61306
|
1864 |
by (auto simp: connected_component_refl) (auto simp: connected_component_def)
|
lp15@61306
|
1865 |
|
lp15@61306
|
1866 |
lemma connected_component_sym: "connected_component s x y \<Longrightarrow> connected_component s y x"
|
lp15@61306
|
1867 |
by (auto simp: connected_component_def)
|
lp15@61306
|
1868 |
|
lp15@61306
|
1869 |
lemma connected_component_trans:
|
lp15@61306
|
1870 |
"\<lbrakk>connected_component s x y; connected_component s y z\<rbrakk> \<Longrightarrow> connected_component s x z"
|
lp15@61306
|
1871 |
unfolding connected_component_def
|
lp15@61306
|
1872 |
by (metis Int_iff Un_iff Un_subset_iff equals0D connected_Un)
|
lp15@61306
|
1873 |
|
lp15@61306
|
1874 |
lemma connected_component_of_subset: "\<lbrakk>connected_component s x y; s \<subseteq> t\<rbrakk> \<Longrightarrow> connected_component t x y"
|
lp15@61306
|
1875 |
by (auto simp: connected_component_def)
|
lp15@61306
|
1876 |
|
lp15@61306
|
1877 |
lemma connected_component_Union: "connected_component_set s x = Union {t. connected t \<and> x \<in> t \<and> t \<subseteq> s}"
|
lp15@61306
|
1878 |
by (auto simp: connected_component_def)
|
lp15@61306
|
1879 |
|
lp15@61306
|
1880 |
lemma connected_connected_component [iff]: "connected (connected_component_set s x)"
|
lp15@61306
|
1881 |
by (auto simp: connected_component_Union intro: connected_Union)
|
lp15@61306
|
1882 |
|
lp15@61306
|
1883 |
lemma connected_iff_eq_connected_component_set: "connected s \<longleftrightarrow> (\<forall>x \<in> s. connected_component_set s x = s)"
|
lp15@61306
|
1884 |
proof (cases "s={}")
|
lp15@61306
|
1885 |
case True then show ?thesis by simp
|
lp15@61306
|
1886 |
next
|
lp15@61306
|
1887 |
case False
|
lp15@61306
|
1888 |
then obtain x where "x \<in> s" by auto
|
lp15@61306
|
1889 |
show ?thesis
|
lp15@61306
|
1890 |
proof
|
lp15@61306
|
1891 |
assume "connected s"
|
lp15@61306
|
1892 |
then show "\<forall>x \<in> s. connected_component_set s x = s"
|
lp15@61306
|
1893 |
by (force simp: connected_component_def)
|
lp15@61306
|
1894 |
next
|
lp15@61306
|
1895 |
assume "\<forall>x \<in> s. connected_component_set s x = s"
|
lp15@61306
|
1896 |
then show "connected s"
|
lp15@61306
|
1897 |
by (metis `x \<in> s` connected_connected_component)
|
lp15@61306
|
1898 |
qed
|
lp15@61306
|
1899 |
qed
|
lp15@61306
|
1900 |
|
lp15@61306
|
1901 |
lemma connected_component_subset: "connected_component_set s x \<subseteq> s"
|
lp15@61306
|
1902 |
using connected_component_in by blast
|
lp15@61306
|
1903 |
|
lp15@61306
|
1904 |
lemma connected_component_eq_self: "\<lbrakk>connected s; x \<in> s\<rbrakk> \<Longrightarrow> connected_component_set s x = s"
|
lp15@61306
|
1905 |
by (simp add: connected_iff_eq_connected_component_set)
|
lp15@61306
|
1906 |
|
lp15@61306
|
1907 |
lemma connected_iff_connected_component:
|
lp15@61306
|
1908 |
"connected s \<longleftrightarrow> (\<forall>x \<in> s. \<forall>y \<in> s. connected_component s x y)"
|
lp15@61306
|
1909 |
using connected_component_in by (auto simp: connected_iff_eq_connected_component_set)
|
lp15@61306
|
1910 |
|
lp15@61306
|
1911 |
lemma connected_component_maximal:
|
lp15@61306
|
1912 |
"\<lbrakk>x \<in> t; connected t; t \<subseteq> s\<rbrakk> \<Longrightarrow> t \<subseteq> (connected_component_set s x)"
|
lp15@61306
|
1913 |
using connected_component_eq_self connected_component_of_subset by blast
|
lp15@61306
|
1914 |
|
lp15@61306
|
1915 |
lemma connected_component_mono:
|
lp15@61306
|
1916 |
"s \<subseteq> t \<Longrightarrow> (connected_component_set s x) \<subseteq> (connected_component_set t x)"
|
lp15@61306
|
1917 |
by (simp add: Collect_mono connected_component_of_subset)
|
lp15@61306
|
1918 |
|
lp15@61306
|
1919 |
lemma connected_component_eq_empty [simp]: "connected_component_set s x = {} \<longleftrightarrow> (x \<notin> s)"
|
lp15@61306
|
1920 |
using connected_component_refl by (fastforce simp: connected_component_in)
|
lp15@61306
|
1921 |
|
lp15@61306
|
1922 |
lemma connected_component_set_empty [simp]: "connected_component_set {} x = {}"
|
lp15@61306
|
1923 |
using connected_component_eq_empty by blast
|
lp15@61306
|
1924 |
|
lp15@61306
|
1925 |
lemma connected_component_eq:
|
lp15@61306
|
1926 |
"y \<in> connected_component_set s x
|
lp15@61306
|
1927 |
\<Longrightarrow> (connected_component_set s y = connected_component_set s x)"
|
lp15@61306
|
1928 |
by (metis (no_types, lifting) Collect_cong connected_component_sym connected_component_trans mem_Collect_eq)
|
lp15@61306
|
1929 |
|
lp15@61306
|
1930 |
lemma closed_connected_component:
|
lp15@61306
|
1931 |
assumes s: "closed s" shows "closed (connected_component_set s x)"
|
lp15@61306
|
1932 |
proof (cases "x \<in> s")
|
lp15@61306
|
1933 |
case False then show ?thesis
|
lp15@61306
|
1934 |
by (metis connected_component_eq_empty closed_empty)
|
lp15@61306
|
1935 |
next
|
lp15@61306
|
1936 |
case True
|
lp15@61306
|
1937 |
show ?thesis
|
lp15@61306
|
1938 |
unfolding closure_eq [symmetric]
|
lp15@61306
|
1939 |
proof
|
lp15@61306
|
1940 |
show "closure (connected_component_set s x) \<subseteq> connected_component_set s x"
|
lp15@61306
|
1941 |
apply (rule connected_component_maximal)
|
lp15@61306
|
1942 |
apply (simp add: closure_def True)
|
lp15@61306
|
1943 |
apply (simp add: connected_imp_connected_closure)
|
lp15@61306
|
1944 |
apply (simp add: s closure_minimal connected_component_subset)
|
lp15@61306
|
1945 |
done
|
lp15@61306
|
1946 |
next
|
lp15@61306
|
1947 |
show "connected_component_set s x \<subseteq> closure (connected_component_set s x)"
|
lp15@61306
|
1948 |
by (simp add: closure_subset)
|
lp15@61306
|
1949 |
qed
|
lp15@61306
|
1950 |
qed
|
lp15@61306
|
1951 |
|
lp15@61306
|
1952 |
lemma connected_component_disjoint:
|
lp15@61306
|
1953 |
"(connected_component_set s a) \<inter> (connected_component_set s b) = {} \<longleftrightarrow>
|
lp15@61306
|
1954 |
a \<notin> connected_component_set s b"
|
lp15@61306
|
1955 |
apply (auto simp: connected_component_eq)
|
lp15@61306
|
1956 |
using connected_component_eq connected_component_sym by blast
|
lp15@61306
|
1957 |
|
lp15@61306
|
1958 |
lemma connected_component_nonoverlap:
|
lp15@61306
|
1959 |
"(connected_component_set s a) \<inter> (connected_component_set s b) = {} \<longleftrightarrow>
|
lp15@61306
|
1960 |
(a \<notin> s \<or> b \<notin> s \<or> connected_component_set s a \<noteq> connected_component_set s b)"
|
lp15@61306
|
1961 |
apply (auto simp: connected_component_in)
|
lp15@61306
|
1962 |
using connected_component_refl_eq apply blast
|
lp15@61306
|
1963 |
apply (metis connected_component_eq mem_Collect_eq)
|
lp15@61306
|
1964 |
apply (metis connected_component_eq mem_Collect_eq)
|
lp15@61306
|
1965 |
done
|
lp15@61306
|
1966 |
|
lp15@61306
|
1967 |
lemma connected_component_overlap:
|
lp15@61306
|
1968 |
"(connected_component_set s a \<inter> connected_component_set s b \<noteq> {}) =
|
lp15@61306
|
1969 |
(a \<in> s \<and> b \<in> s \<and> connected_component_set s a = connected_component_set s b)"
|
lp15@61306
|
1970 |
by (auto simp: connected_component_nonoverlap)
|
lp15@61306
|
1971 |
|
lp15@61306
|
1972 |
lemma connected_component_sym_eq: "connected_component s x y \<longleftrightarrow> connected_component s y x"
|
lp15@61306
|
1973 |
using connected_component_sym by blast
|
lp15@61306
|
1974 |
|
lp15@61306
|
1975 |
lemma connected_component_eq_eq:
|
lp15@61306
|
1976 |
"connected_component_set s x = connected_component_set s y \<longleftrightarrow>
|
lp15@61306
|
1977 |
x \<notin> s \<and> y \<notin> s \<or> x \<in> s \<and> y \<in> s \<and> connected_component s x y"
|
lp15@61306
|
1978 |
apply (case_tac "y \<in> s")
|
lp15@61306
|
1979 |
apply (simp add:)
|
lp15@61306
|
1980 |
apply (metis connected_component_eq connected_component_eq_empty connected_component_refl_eq mem_Collect_eq)
|
lp15@61306
|
1981 |
apply (case_tac "x \<in> s")
|
lp15@61306
|
1982 |
apply (simp add:)
|
lp15@61306
|
1983 |
apply (metis connected_component_eq_empty)
|
lp15@61306
|
1984 |
using connected_component_eq_empty by blast
|
lp15@61306
|
1985 |
|
lp15@61306
|
1986 |
lemma connected_iff_connected_component_eq:
|
lp15@61306
|
1987 |
"connected s \<longleftrightarrow>
|
lp15@61306
|
1988 |
(\<forall>x \<in> s. \<forall>y \<in> s. connected_component_set s x = connected_component_set s y)"
|
lp15@61306
|
1989 |
by (simp add: connected_component_eq_eq connected_iff_connected_component)
|
lp15@61306
|
1990 |
|
lp15@61306
|
1991 |
lemma connected_component_idemp:
|
lp15@61306
|
1992 |
"connected_component_set (connected_component_set s x) x = connected_component_set s x"
|
lp15@61306
|
1993 |
apply (rule subset_antisym)
|
lp15@61306
|
1994 |
apply (simp add: connected_component_subset)
|
lp15@61306
|
1995 |
by (metis connected_component_eq_empty connected_component_maximal connected_component_refl_eq connected_connected_component mem_Collect_eq set_eq_subset)
|
lp15@61306
|
1996 |
|
lp15@61306
|
1997 |
lemma connected_component_unique:
|
lp15@61306
|
1998 |
"\<lbrakk>x \<in> c; c \<subseteq> s; connected c;
|
lp15@61306
|
1999 |
\<And>c'. x \<in> c' \<and> c' \<subseteq> s \<and> connected c'
|
lp15@61306
|
2000 |
\<Longrightarrow> c' \<subseteq> c\<rbrakk>
|
lp15@61306
|
2001 |
\<Longrightarrow> connected_component_set s x = c"
|
lp15@61306
|
2002 |
apply (rule subset_antisym)
|
lp15@61306
|
2003 |
apply (meson connected_component_maximal connected_component_subset connected_connected_component contra_subsetD)
|
lp15@61306
|
2004 |
by (simp add: connected_component_maximal)
|
lp15@61306
|
2005 |
|
lp15@61306
|
2006 |
lemma joinable_connected_component_eq:
|
lp15@61306
|
2007 |
"\<lbrakk>connected t; t \<subseteq> s;
|
lp15@61306
|
2008 |
connected_component_set s x \<inter> t \<noteq> {};
|
lp15@61306
|
2009 |
connected_component_set s y \<inter> t \<noteq> {}\<rbrakk>
|
lp15@61306
|
2010 |
\<Longrightarrow> connected_component_set s x = connected_component_set s y"
|
lp15@61306
|
2011 |
apply (simp add: ex_in_conv [symmetric])
|
lp15@61306
|
2012 |
apply (rule connected_component_eq)
|
lp15@61306
|
2013 |
by (metis (no_types, hide_lams) connected_component_eq_eq connected_component_in connected_component_maximal subsetD mem_Collect_eq)
|
lp15@61306
|
2014 |
|
lp15@61306
|
2015 |
|
lp15@61306
|
2016 |
lemma Union_connected_component: "Union (connected_component_set s ` s) = s"
|
lp15@61306
|
2017 |
apply (rule subset_antisym)
|
lp15@61306
|
2018 |
apply (simp add: SUP_least connected_component_subset)
|
lp15@61306
|
2019 |
using connected_component_refl_eq
|
lp15@61306
|
2020 |
by force
|
lp15@61306
|
2021 |
|
lp15@61306
|
2022 |
|
lp15@61306
|
2023 |
lemma complement_connected_component_unions:
|
lp15@61306
|
2024 |
"s - connected_component_set s x =
|
lp15@61306
|
2025 |
Union (connected_component_set s ` s - {connected_component_set s x})"
|
lp15@61306
|
2026 |
apply (subst Union_connected_component [symmetric], auto)
|
lp15@61306
|
2027 |
apply (metis connected_component_eq_eq connected_component_in)
|
lp15@61306
|
2028 |
by (metis connected_component_eq mem_Collect_eq)
|
lp15@61306
|
2029 |
|
lp15@61306
|
2030 |
lemma connected_component_intermediate_subset:
|
lp15@61306
|
2031 |
"\<lbrakk>connected_component_set u a \<subseteq> t; t \<subseteq> u\<rbrakk>
|
lp15@61306
|
2032 |
\<Longrightarrow> connected_component_set t a = connected_component_set u a"
|
lp15@61306
|
2033 |
apply (case_tac "a \<in> u")
|
lp15@61306
|
2034 |
apply (simp add: connected_component_maximal connected_component_mono subset_antisym)
|
lp15@61306
|
2035 |
using connected_component_eq_empty by blast
|
lp15@61306
|
2036 |
|
lp15@61306
|
2037 |
subsection\<open>The set of connected components of a set\<close>
|
lp15@61306
|
2038 |
|
lp15@61306
|
2039 |
definition components:: "'a::topological_space set \<Rightarrow> 'a set set" where
|
lp15@61306
|
2040 |
"components s \<equiv> connected_component_set s ` s"
|
lp15@61306
|
2041 |
|
lp15@61306
|
2042 |
lemma components_iff: "s \<in> components u \<longleftrightarrow> (\<exists>x. x \<in> u \<and> s = connected_component_set u x)"
|
lp15@61306
|
2043 |
by (auto simp: components_def)
|
lp15@61306
|
2044 |
|
lp15@61306
|
2045 |
lemma Union_components: "u = Union (components u)"
|
lp15@61306
|
2046 |
apply (rule subset_antisym)
|
lp15@61306
|
2047 |
apply (metis Union_connected_component components_def set_eq_subset)
|
lp15@61306
|
2048 |
using Union_connected_component components_def by fastforce
|
lp15@61306
|
2049 |
|
lp15@61306
|
2050 |
lemma pairwise_disjoint_components: "pairwise (\<lambda>X Y. X \<inter> Y = {}) (components u)"
|
lp15@61306
|
2051 |
apply (simp add: pairwise_def)
|
lp15@61306
|
2052 |
apply (auto simp: components_iff)
|
lp15@61306
|
2053 |
apply (metis connected_component_eq_eq connected_component_in)+
|
lp15@61306
|
2054 |
done
|
lp15@61306
|
2055 |
|
lp15@61306
|
2056 |
lemma in_components_nonempty: "c \<in> components s \<Longrightarrow> c \<noteq> {}"
|
lp15@61306
|
2057 |
by (metis components_iff connected_component_eq_empty)
|
lp15@61306
|
2058 |
|
lp15@61306
|
2059 |
lemma in_components_subset: "c \<in> components s \<Longrightarrow> c \<subseteq> s"
|
lp15@61306
|
2060 |
using Union_components by blast
|
lp15@61306
|
2061 |
|
lp15@61306
|
2062 |
lemma in_components_connected: "c \<in> components s \<Longrightarrow> connected c"
|
lp15@61306
|
2063 |
by (metis components_iff connected_connected_component)
|
lp15@61306
|
2064 |
|
lp15@61306
|
2065 |
lemma in_components_maximal:
|
lp15@61306
|
2066 |
"c \<in> components s \<longleftrightarrow>
|
lp15@61306
|
2067 |
(c \<noteq> {} \<and> c \<subseteq> s \<and> connected c \<and> (\<forall>d. d \<noteq> {} \<and> c \<subseteq> d \<and> d \<subseteq> s \<and> connected d \<longrightarrow> d = c))"
|
lp15@61306
|
2068 |
apply (rule iffI)
|
lp15@61306
|
2069 |
apply (simp add: in_components_nonempty in_components_connected)
|
lp15@61306
|
2070 |
apply (metis (full_types) components_iff connected_component_eq_self connected_component_intermediate_subset connected_component_refl in_components_subset mem_Collect_eq rev_subsetD)
|
lp15@61306
|
2071 |
by (metis bot.extremum_uniqueI components_iff connected_component_eq_empty connected_component_maximal connected_component_subset connected_connected_component subset_emptyI)
|
lp15@61306
|
2072 |
|
lp15@61306
|
2073 |
lemma joinable_components_eq:
|
lp15@61306
|
2074 |
"connected t \<and> t \<subseteq> s \<and> c1 \<in> components s \<and> c2 \<in> components s \<and> c1 \<inter> t \<noteq> {} \<and> c2 \<inter> t \<noteq> {} \<Longrightarrow> c1 = c2"
|
lp15@61306
|
2075 |
by (metis (full_types) components_iff joinable_connected_component_eq)
|
lp15@61306
|
2076 |
|
lp15@61306
|
2077 |
lemma closed_components: "\<lbrakk>closed s; c \<in> components s\<rbrakk> \<Longrightarrow> closed c"
|
lp15@61306
|
2078 |
by (metis closed_connected_component components_iff)
|
lp15@61306
|
2079 |
|
lp15@61306
|
2080 |
lemma components_nonoverlap:
|
lp15@61306
|
2081 |
"\<lbrakk>c \<in> components s; c' \<in> components s\<rbrakk> \<Longrightarrow> (c \<inter> c' = {}) \<longleftrightarrow> (c \<noteq> c')"
|
lp15@61306
|
2082 |
apply (auto simp: in_components_nonempty components_iff)
|
lp15@61306
|
2083 |
using connected_component_refl apply blast
|
lp15@61306
|
2084 |
apply (metis connected_component_eq_eq connected_component_in)
|
lp15@61306
|
2085 |
by (metis connected_component_eq mem_Collect_eq)
|
lp15@61306
|
2086 |
|
lp15@61306
|
2087 |
lemma components_eq: "\<lbrakk>c \<in> components s; c' \<in> components s\<rbrakk> \<Longrightarrow> (c = c' \<longleftrightarrow> c \<inter> c' \<noteq> {})"
|
lp15@61306
|
2088 |
by (metis components_nonoverlap)
|
lp15@61306
|
2089 |
|
lp15@61306
|
2090 |
lemma components_eq_empty [simp]: "components s = {} \<longleftrightarrow> s = {}"
|
lp15@61306
|
2091 |
by (simp add: components_def)
|
lp15@61306
|
2092 |
|
lp15@61306
|
2093 |
lemma components_empty [simp]: "components {} = {}"
|
lp15@61306
|
2094 |
by simp
|
lp15@61306
|
2095 |
|
lp15@61306
|
2096 |
lemma connected_eq_connected_components_eq: "connected s \<longleftrightarrow> (\<forall>c \<in> components s. \<forall>c' \<in> components s. c = c')"
|
lp15@61306
|
2097 |
by (metis (no_types, hide_lams) components_iff connected_component_eq_eq connected_iff_connected_component)
|
lp15@61306
|
2098 |
|
lp15@61306
|
2099 |
lemma components_eq_sing_iff: "components s = {s} \<longleftrightarrow> connected s \<and> s \<noteq> {}"
|
lp15@61306
|
2100 |
apply (rule iffI)
|
lp15@61306
|
2101 |
using in_components_connected apply fastforce
|
lp15@61306
|
2102 |
apply safe
|
lp15@61306
|
2103 |
using Union_components apply fastforce
|
lp15@61306
|
2104 |
apply (metis components_iff connected_component_eq_self)
|
lp15@61306
|
2105 |
using in_components_maximal by auto
|
lp15@61306
|
2106 |
|
lp15@61306
|
2107 |
lemma components_eq_sing_exists: "(\<exists>a. components s = {a}) \<longleftrightarrow> connected s \<and> s \<noteq> {}"
|
lp15@61306
|
2108 |
apply (rule iffI)
|
lp15@61306
|
2109 |
using connected_eq_connected_components_eq apply fastforce
|
lp15@61306
|
2110 |
by (metis components_eq_sing_iff)
|
lp15@61306
|
2111 |
|
lp15@61306
|
2112 |
lemma connected_eq_components_subset_sing: "connected s \<longleftrightarrow> components s \<subseteq> {s}"
|
lp15@61306
|
2113 |
by (metis Union_components components_empty components_eq_sing_iff connected_empty insert_subset order_refl subset_singletonD)
|
lp15@61306
|
2114 |
|
lp15@61306
|
2115 |
lemma connected_eq_components_subset_sing_exists: "connected s \<longleftrightarrow> (\<exists>a. components s \<subseteq> {a})"
|
lp15@61306
|
2116 |
by (metis components_eq_sing_exists connected_eq_components_subset_sing empty_iff subset_iff subset_singletonD)
|
lp15@61306
|
2117 |
|
lp15@61306
|
2118 |
lemma in_components_self: "s \<in> components s \<longleftrightarrow> connected s \<and> s \<noteq> {}"
|
lp15@61306
|
2119 |
by (metis components_empty components_eq_sing_iff empty_iff in_components_connected insertI1)
|
lp15@61306
|
2120 |
|
lp15@61306
|
2121 |
lemma components_maximal: "\<lbrakk>c \<in> components s; connected t; t \<subseteq> s; c \<inter> t \<noteq> {}\<rbrakk> \<Longrightarrow> t \<subseteq> c"
|
lp15@61306
|
2122 |
apply (simp add: components_def ex_in_conv [symmetric], clarify)
|
lp15@61306
|
2123 |
by (meson connected_component_def connected_component_trans)
|
lp15@61306
|
2124 |
|
lp15@61306
|
2125 |
lemma exists_component_superset: "\<lbrakk>t \<subseteq> s; s \<noteq> {}; connected t\<rbrakk> \<Longrightarrow> \<exists>c. c \<in> components s \<and> t \<subseteq> c"
|
lp15@61306
|
2126 |
apply (case_tac "t = {}")
|
lp15@61306
|
2127 |
apply force
|
lp15@61306
|
2128 |
by (metis components_def ex_in_conv connected_component_maximal contra_subsetD image_eqI)
|
lp15@61306
|
2129 |
|
lp15@61306
|
2130 |
lemma components_intermediate_subset: "\<lbrakk>s \<in> components u; s \<subseteq> t; t \<subseteq> u\<rbrakk> \<Longrightarrow> s \<in> components t"
|
lp15@61306
|
2131 |
apply (auto simp: components_iff)
|
lp15@61306
|
2132 |
by (metis connected_component_eq_empty connected_component_intermediate_subset)
|
lp15@61306
|
2133 |
|
lp15@61306
|
2134 |
lemma in_components_unions_complement: "c \<in> components s \<Longrightarrow> s - c = Union(components s - {c})"
|
lp15@61306
|
2135 |
by (metis complement_connected_component_unions components_def components_iff)
|
lp15@61306
|
2136 |
|
lp15@61306
|
2137 |
lemma connected_intermediate_closure:
|
lp15@61306
|
2138 |
assumes cs: "connected s" and st: "s \<subseteq> t" and ts: "t \<subseteq> closure s"
|
lp15@61306
|
2139 |
shows "connected t"
|
lp15@61306
|
2140 |
proof (rule connectedI)
|
lp15@61306
|
2141 |
fix A B
|
lp15@61306
|
2142 |
assume A: "open A" and B: "open B" and Alap: "A \<inter> t \<noteq> {}" and Blap: "B \<inter> t \<noteq> {}"
|
lp15@61306
|
2143 |
and disj: "A \<inter> B \<inter> t = {}" and cover: "t \<subseteq> A \<union> B"
|
lp15@61306
|
2144 |
have disjs: "A \<inter> B \<inter> s = {}"
|
lp15@61306
|
2145 |
using disj st by auto
|
lp15@61306
|
2146 |
have "A \<inter> closure s \<noteq> {}"
|
lp15@61306
|
2147 |
using Alap Int_absorb1 ts by blast
|
lp15@61306
|
2148 |
then have Alaps: "A \<inter> s \<noteq> {}"
|
lp15@61306
|
2149 |
by (simp add: A open_inter_closure_eq_empty)
|
lp15@61306
|
2150 |
have "B \<inter> closure s \<noteq> {}"
|
lp15@61306
|
2151 |
using Blap Int_absorb1 ts by blast
|
lp15@61306
|
2152 |
then have Blaps: "B \<inter> s \<noteq> {}"
|
lp15@61306
|
2153 |
by (simp add: B open_inter_closure_eq_empty)
|
lp15@61306
|
2154 |
then show False
|
lp15@61306
|
2155 |
using cs [unfolded connected_def] A B disjs Alaps Blaps cover st
|
lp15@61306
|
2156 |
by blast
|
lp15@61306
|
2157 |
qed
|
lp15@61306
|
2158 |
|
lp15@61306
|
2159 |
lemma closed_in_connected_component: "closedin (subtopology euclidean s) (connected_component_set s x)"
|
lp15@61306
|
2160 |
proof (cases "connected_component_set s x = {}")
|
lp15@61609
|
2161 |
case True then show ?thesis
|
lp15@61306
|
2162 |
by (metis closedin_empty)
|
lp15@61306
|
2163 |
next
|
lp15@61306
|
2164 |
case False
|
lp15@61306
|
2165 |
then obtain y where y: "connected_component s x y"
|
lp15@61306
|
2166 |
by blast
|
lp15@61306
|
2167 |
have 1: "connected_component_set s x \<subseteq> s \<inter> closure (connected_component_set s x)"
|
lp15@61306
|
2168 |
by (auto simp: closure_def connected_component_in)
|
lp15@61306
|
2169 |
have 2: "connected_component s x y \<Longrightarrow> s \<inter> closure (connected_component_set s x) \<subseteq> connected_component_set s x"
|
lp15@61306
|
2170 |
apply (rule connected_component_maximal)
|
lp15@61306
|
2171 |
apply (simp add:)
|
lp15@61306
|
2172 |
using closure_subset connected_component_in apply fastforce
|
lp15@61306
|
2173 |
using "1" connected_intermediate_closure apply blast+
|
lp15@61306
|
2174 |
done
|
lp15@61306
|
2175 |
show ?thesis using y
|
lp15@61306
|
2176 |
apply (simp add: Topology_Euclidean_Space.closedin_closed)
|
lp15@61306
|
2177 |
using 1 2 by auto
|
lp15@61306
|
2178 |
qed
|
hoelzl@51351
|
2179 |
|
wenzelm@60420
|
2180 |
subsection \<open>Frontier (aka boundary)\<close>
|
himmelma@33175
|
2181 |
|
himmelma@33175
|
2182 |
definition "frontier S = closure S - interior S"
|
himmelma@33175
|
2183 |
|
wenzelm@53255
|
2184 |
lemma frontier_closed: "closed (frontier S)"
|
himmelma@33175
|
2185 |
by (simp add: frontier_def closed_Diff)
|
himmelma@33175
|
2186 |
|
huffman@34105
|
2187 |
lemma frontier_closures: "frontier S = (closure S) \<inter> (closure(- S))"
|
himmelma@33175
|
2188 |
by (auto simp add: frontier_def interior_closure)
|
himmelma@33175
|
2189 |
|
himmelma@33175
|
2190 |
lemma frontier_straddle:
|
himmelma@33175
|
2191 |
fixes a :: "'a::metric_space"
|
huffman@44909
|
2192 |
shows "a \<in> frontier S \<longleftrightarrow> (\<forall>e>0. (\<exists>x\<in>S. dist a x < e) \<and> (\<exists>x. x \<notin> S \<and> dist a x < e))"
|
huffman@44909
|
2193 |
unfolding frontier_def closure_interior
|
huffman@44909
|
2194 |
by (auto simp add: mem_interior subset_eq ball_def)
|
himmelma@33175
|
2195 |
|
himmelma@33175
|
2196 |
lemma frontier_subset_closed: "closed S \<Longrightarrow> frontier S \<subseteq> S"
|
himmelma@33175
|
2197 |
by (metis frontier_def closure_closed Diff_subset)
|
himmelma@33175
|
2198 |
|
hoelzl@34964
|
2199 |
lemma frontier_empty[simp]: "frontier {} = {}"
|
huffman@36362
|
2200 |
by (simp add: frontier_def)
|
himmelma@33175
|
2201 |
|
himmelma@33175
|
2202 |
lemma frontier_subset_eq: "frontier S \<subseteq> S \<longleftrightarrow> closed S"
|
wenzelm@58757
|
2203 |
proof -
|
wenzelm@53255
|
2204 |
{
|
wenzelm@53255
|
2205 |
assume "frontier S \<subseteq> S"
|
wenzelm@53255
|
2206 |
then have "closure S \<subseteq> S"
|
wenzelm@53255
|
2207 |
using interior_subset unfolding frontier_def by auto
|
wenzelm@53255
|
2208 |
then have "closed S"
|
wenzelm@53255
|
2209 |
using closure_subset_eq by auto
|
himmelma@33175
|
2210 |
}
|
wenzelm@53255
|
2211 |
then show ?thesis using frontier_subset_closed[of S] ..
|
himmelma@33175
|
2212 |
qed
|
himmelma@33175
|
2213 |
|
paulson@61518
|
2214 |
lemma frontier_complement [simp]: "frontier (- S) = frontier S"
|
himmelma@33175
|
2215 |
by (auto simp add: frontier_def closure_complement interior_complement)
|
himmelma@33175
|
2216 |
|
himmelma@33175
|
2217 |
lemma frontier_disjoint_eq: "frontier S \<inter> S = {} \<longleftrightarrow> open S"
|
huffman@34105
|
2218 |
using frontier_complement frontier_subset_eq[of "- S"]
|
huffman@34105
|
2219 |
unfolding open_closed by auto
|
himmelma@33175
|
2220 |
|
wenzelm@58757
|
2221 |
|
wenzelm@60420
|
2222 |
subsection \<open>Filters and the ``eventually true'' quantifier\<close>
|
huffman@44081
|
2223 |
|
wenzelm@52624
|
2224 |
definition indirection :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> 'a filter"
|
wenzelm@52624
|
2225 |
(infixr "indirection" 70)
|
wenzelm@52624
|
2226 |
where "a indirection v = at a within {b. \<exists>c\<ge>0. b - a = scaleR c v}"
|
himmelma@33175
|
2227 |
|
wenzelm@60420
|
2228 |
text \<open>Identify Trivial limits, where we can't approach arbitrarily closely.\<close>
|
himmelma@33175
|
2229 |
|
wenzelm@52624
|
2230 |
lemma trivial_limit_within: "trivial_limit (at a within S) \<longleftrightarrow> \<not> a islimpt S"
|
himmelma@33175
|
2231 |
proof
|
himmelma@33175
|
2232 |
assume "trivial_limit (at a within S)"
|
wenzelm@53255
|
2233 |
then show "\<not> a islimpt S"
|
himmelma@33175
|
2234 |
unfolding trivial_limit_def
|
|