author | immler |
Tue, 18 Mar 2014 10:12:57 +0100 | |
changeset 56188 | 0268784f60da |
parent 56166 | 9a241bc276cd |
child 56189 | c4daa97ac57a |
permissions | -rw-r--r-- |
33714
eb2574ac4173
Added new lemmas to Euclidean Space by Robert Himmelmann
hoelzl
parents:
33324
diff
changeset
|
1 |
(* title: HOL/Library/Topology_Euclidian_Space.thy |
33175 | 2 |
Author: Amine Chaieb, University of Cambridge |
3 |
Author: Robert Himmelmann, TU Muenchen |
|
44075 | 4 |
Author: Brian Huffman, Portland State University |
33175 | 5 |
*) |
6 |
||
7 |
header {* Elementary topology in Euclidean space. *} |
|
8 |
||
9 |
theory Topology_Euclidean_Space |
|
50087 | 10 |
imports |
50938 | 11 |
Complex_Main |
50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset
|
12 |
"~~/src/HOL/Library/Countable_Set" |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
13 |
"~~/src/HOL/Library/FuncSet" |
50938 | 14 |
Linear_Algebra |
50087 | 15 |
Norm_Arith |
16 |
begin |
|
17 |
||
50972 | 18 |
lemma dist_0_norm: |
19 |
fixes x :: "'a::real_normed_vector" |
|
20 |
shows "dist 0 x = norm x" |
|
21 |
unfolding dist_norm by simp |
|
22 |
||
50943
88a00a1c7c2c
use accumulation point characterization (avoids t1_space restriction for equivalence of countable and sequential compactness); remove heine_borel_lemma
hoelzl
parents:
50942
diff
changeset
|
23 |
lemma dist_double: "dist x y < d / 2 \<Longrightarrow> dist x z < d / 2 \<Longrightarrow> dist y z < d" |
88a00a1c7c2c
use accumulation point characterization (avoids t1_space restriction for equivalence of countable and sequential compactness); remove heine_borel_lemma
hoelzl
parents:
50942
diff
changeset
|
24 |
using dist_triangle[of y z x] by (simp add: dist_commute) |
88a00a1c7c2c
use accumulation point characterization (avoids t1_space restriction for equivalence of countable and sequential compactness); remove heine_borel_lemma
hoelzl
parents:
50942
diff
changeset
|
25 |
|
50972 | 26 |
(* LEGACY *) |
53640 | 27 |
lemma lim_subseq: "subseq r \<Longrightarrow> s ----> l \<Longrightarrow> (s \<circ> r) ----> l" |
50972 | 28 |
by (rule LIMSEQ_subseq_LIMSEQ) |
29 |
||
53282 | 30 |
lemma countable_PiE: |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
31 |
"finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (PiE I F)" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
32 |
by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq) |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
33 |
|
51481
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset
|
34 |
lemma Lim_within_open: |
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset
|
35 |
fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space" |
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset
|
36 |
shows "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f ---> l)(at a within S) \<longleftrightarrow> (f ---> l)(at a)" |
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset
|
37 |
by (fact tendsto_within_open) |
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset
|
38 |
|
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset
|
39 |
lemma continuous_on_union: |
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset
|
40 |
"closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f" |
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset
|
41 |
by (fact continuous_on_closed_Un) |
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset
|
42 |
|
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset
|
43 |
lemma continuous_on_cases: |
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset
|
44 |
"closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t g \<Longrightarrow> |
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset
|
45 |
\<forall>x. (x\<in>s \<and> \<not> P x) \<or> (x \<in> t \<and> P x) \<longrightarrow> f x = g x \<Longrightarrow> |
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset
|
46 |
continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)" |
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset
|
47 |
by (rule continuous_on_If) auto |
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset
|
48 |
|
53255 | 49 |
|
50087 | 50 |
subsection {* Topological Basis *} |
51 |
||
52 |
context topological_space |
|
53 |
begin |
|
54 |
||
53291 | 55 |
definition "topological_basis B \<longleftrightarrow> |
56 |
(\<forall>b\<in>B. open b) \<and> (\<forall>x. open x \<longrightarrow> (\<exists>B'. B' \<subseteq> B \<and> \<Union>B' = x))" |
|
51343
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
57 |
|
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
58 |
lemma topological_basis: |
53291 | 59 |
"topological_basis B \<longleftrightarrow> (\<forall>x. open x \<longleftrightarrow> (\<exists>B'. B' \<subseteq> B \<and> \<Union>B' = x))" |
50998 | 60 |
unfolding topological_basis_def |
61 |
apply safe |
|
62 |
apply fastforce |
|
63 |
apply fastforce |
|
64 |
apply (erule_tac x="x" in allE) |
|
65 |
apply simp |
|
66 |
apply (rule_tac x="{x}" in exI) |
|
67 |
apply auto |
|
68 |
done |
|
69 |
||
50087 | 70 |
lemma topological_basis_iff: |
71 |
assumes "\<And>B'. B' \<in> B \<Longrightarrow> open B'" |
|
72 |
shows "topological_basis B \<longleftrightarrow> (\<forall>O'. open O' \<longrightarrow> (\<forall>x\<in>O'. \<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'))" |
|
73 |
(is "_ \<longleftrightarrow> ?rhs") |
|
74 |
proof safe |
|
75 |
fix O' and x::'a |
|
76 |
assume H: "topological_basis B" "open O'" "x \<in> O'" |
|
53282 | 77 |
then have "(\<exists>B'\<subseteq>B. \<Union>B' = O')" by (simp add: topological_basis_def) |
50087 | 78 |
then obtain B' where "B' \<subseteq> B" "O' = \<Union>B'" by auto |
53282 | 79 |
then show "\<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'" using H by auto |
50087 | 80 |
next |
81 |
assume H: ?rhs |
|
53282 | 82 |
show "topological_basis B" |
83 |
using assms unfolding topological_basis_def |
|
50087 | 84 |
proof safe |
53640 | 85 |
fix O' :: "'a set" |
53282 | 86 |
assume "open O'" |
50087 | 87 |
with H obtain f where "\<forall>x\<in>O'. f x \<in> B \<and> x \<in> f x \<and> f x \<subseteq> O'" |
88 |
by (force intro: bchoice simp: Bex_def) |
|
53282 | 89 |
then show "\<exists>B'\<subseteq>B. \<Union>B' = O'" |
50087 | 90 |
by (auto intro: exI[where x="{f x |x. x \<in> O'}"]) |
91 |
qed |
|
92 |
qed |
|
93 |
||
94 |
lemma topological_basisI: |
|
95 |
assumes "\<And>B'. B' \<in> B \<Longrightarrow> open B'" |
|
53282 | 96 |
and "\<And>O' x. open O' \<Longrightarrow> x \<in> O' \<Longrightarrow> \<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'" |
50087 | 97 |
shows "topological_basis B" |
98 |
using assms by (subst topological_basis_iff) auto |
|
99 |
||
100 |
lemma topological_basisE: |
|
101 |
fixes O' |
|
102 |
assumes "topological_basis B" |
|
53282 | 103 |
and "open O'" |
104 |
and "x \<in> O'" |
|
50087 | 105 |
obtains B' where "B' \<in> B" "x \<in> B'" "B' \<subseteq> O'" |
106 |
proof atomize_elim |
|
53282 | 107 |
from assms have "\<And>B'. B'\<in>B \<Longrightarrow> open B'" |
108 |
by (simp add: topological_basis_def) |
|
50087 | 109 |
with topological_basis_iff assms |
53282 | 110 |
show "\<exists>B'. B' \<in> B \<and> x \<in> B' \<and> B' \<subseteq> O'" |
111 |
using assms by (simp add: Bex_def) |
|
50087 | 112 |
qed |
113 |
||
50094
84ddcf5364b4
allow arbitrary enumerations of basis in locale for generation of borel sets
immler
parents:
50087
diff
changeset
|
114 |
lemma topological_basis_open: |
84ddcf5364b4
allow arbitrary enumerations of basis in locale for generation of borel sets
immler
parents:
50087
diff
changeset
|
115 |
assumes "topological_basis B" |
53282 | 116 |
and "X \<in> B" |
50094
84ddcf5364b4
allow arbitrary enumerations of basis in locale for generation of borel sets
immler
parents:
50087
diff
changeset
|
117 |
shows "open X" |
53282 | 118 |
using assms by (simp add: topological_basis_def) |
50094
84ddcf5364b4
allow arbitrary enumerations of basis in locale for generation of borel sets
immler
parents:
50087
diff
changeset
|
119 |
|
51343
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
120 |
lemma topological_basis_imp_subbasis: |
53255 | 121 |
assumes B: "topological_basis B" |
122 |
shows "open = generate_topology B" |
|
51343
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
123 |
proof (intro ext iffI) |
53255 | 124 |
fix S :: "'a set" |
125 |
assume "open S" |
|
51343
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
126 |
with B obtain B' where "B' \<subseteq> B" "S = \<Union>B'" |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
127 |
unfolding topological_basis_def by blast |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
128 |
then show "generate_topology B S" |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
129 |
by (auto intro: generate_topology.intros dest: topological_basis_open) |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
130 |
next |
53255 | 131 |
fix S :: "'a set" |
132 |
assume "generate_topology B S" |
|
133 |
then show "open S" |
|
51343
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
134 |
by induct (auto dest: topological_basis_open[OF B]) |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
135 |
qed |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
136 |
|
50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset
|
137 |
lemma basis_dense: |
53640 | 138 |
fixes B :: "'a set set" |
139 |
and f :: "'a set \<Rightarrow> 'a" |
|
50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset
|
140 |
assumes "topological_basis B" |
53255 | 141 |
and choosefrom_basis: "\<And>B'. B' \<noteq> {} \<Longrightarrow> f B' \<in> B'" |
55522 | 142 |
shows "\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>B' \<in> B. f B' \<in> X)" |
50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset
|
143 |
proof (intro allI impI) |
53640 | 144 |
fix X :: "'a set" |
145 |
assume "open X" and "X \<noteq> {}" |
|
50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset
|
146 |
from topological_basisE[OF `topological_basis B` `open X` choosefrom_basis[OF `X \<noteq> {}`]] |
55522 | 147 |
obtain B' where "B' \<in> B" "f X \<in> B'" "B' \<subseteq> X" . |
53255 | 148 |
then show "\<exists>B'\<in>B. f B' \<in> X" |
149 |
by (auto intro!: choosefrom_basis) |
|
50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset
|
150 |
qed |
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset
|
151 |
|
50087 | 152 |
end |
153 |
||
50882
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset
|
154 |
lemma topological_basis_prod: |
53255 | 155 |
assumes A: "topological_basis A" |
156 |
and B: "topological_basis B" |
|
50882
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset
|
157 |
shows "topological_basis ((\<lambda>(a, b). a \<times> b) ` (A \<times> B))" |
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset
|
158 |
unfolding topological_basis_def |
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset
|
159 |
proof (safe, simp_all del: ex_simps add: subset_image_iff ex_simps(1)[symmetric]) |
53255 | 160 |
fix S :: "('a \<times> 'b) set" |
161 |
assume "open S" |
|
50882
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset
|
162 |
then show "\<exists>X\<subseteq>A \<times> B. (\<Union>(a,b)\<in>X. a \<times> b) = S" |
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset
|
163 |
proof (safe intro!: exI[of _ "{x\<in>A \<times> B. fst x \<times> snd x \<subseteq> S}"]) |
53255 | 164 |
fix x y |
165 |
assume "(x, y) \<in> S" |
|
50882
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset
|
166 |
from open_prod_elim[OF `open S` this] |
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset
|
167 |
obtain a b where a: "open a""x \<in> a" and b: "open b" "y \<in> b" and "a \<times> b \<subseteq> S" |
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset
|
168 |
by (metis mem_Sigma_iff) |
55522 | 169 |
moreover |
170 |
from A a obtain A0 where "A0 \<in> A" "x \<in> A0" "A0 \<subseteq> a" |
|
171 |
by (rule topological_basisE) |
|
172 |
moreover |
|
173 |
from B b obtain B0 where "B0 \<in> B" "y \<in> B0" "B0 \<subseteq> b" |
|
174 |
by (rule topological_basisE) |
|
50882
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset
|
175 |
ultimately show "(x, y) \<in> (\<Union>(a, b)\<in>{X \<in> A \<times> B. fst X \<times> snd X \<subseteq> S}. a \<times> b)" |
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset
|
176 |
by (intro UN_I[of "(A0, B0)"]) auto |
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset
|
177 |
qed auto |
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset
|
178 |
qed (metis A B topological_basis_open open_Times) |
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset
|
179 |
|
53255 | 180 |
|
50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset
|
181 |
subsection {* Countable Basis *} |
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset
|
182 |
|
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset
|
183 |
locale countable_basis = |
53640 | 184 |
fixes B :: "'a::topological_space set set" |
50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset
|
185 |
assumes is_basis: "topological_basis B" |
53282 | 186 |
and countable_basis: "countable B" |
33175 | 187 |
begin |
188 |
||
50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset
|
189 |
lemma open_countable_basis_ex: |
50087 | 190 |
assumes "open X" |
50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset
|
191 |
shows "\<exists>B' \<subseteq> B. X = Union B'" |
53255 | 192 |
using assms countable_basis is_basis |
193 |
unfolding topological_basis_def by blast |
|
50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset
|
194 |
|
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset
|
195 |
lemma open_countable_basisE: |
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset
|
196 |
assumes "open X" |
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset
|
197 |
obtains B' where "B' \<subseteq> B" "X = Union B'" |
53255 | 198 |
using assms open_countable_basis_ex |
199 |
by (atomize_elim) simp |
|
50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset
|
200 |
|
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset
|
201 |
lemma countable_dense_exists: |
53291 | 202 |
"\<exists>D::'a set. countable D \<and> (\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>d \<in> D. d \<in> X))" |
50087 | 203 |
proof - |
50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset
|
204 |
let ?f = "(\<lambda>B'. SOME x. x \<in> B')" |
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset
|
205 |
have "countable (?f ` B)" using countable_basis by simp |
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset
|
206 |
with basis_dense[OF is_basis, of ?f] show ?thesis |
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset
|
207 |
by (intro exI[where x="?f ` B"]) (metis (mono_tags) all_not_in_conv imageI someI) |
50087 | 208 |
qed |
209 |
||
210 |
lemma countable_dense_setE: |
|
50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset
|
211 |
obtains D :: "'a set" |
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset
|
212 |
where "countable D" "\<And>X. open X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> \<exists>d \<in> D. d \<in> X" |
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset
|
213 |
using countable_dense_exists by blast |
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset
|
214 |
|
50087 | 215 |
end |
216 |
||
50883 | 217 |
lemma (in first_countable_topology) first_countable_basisE: |
218 |
obtains A where "countable A" "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a" |
|
219 |
"\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)" |
|
220 |
using first_countable_basis[of x] |
|
51473 | 221 |
apply atomize_elim |
222 |
apply (elim exE) |
|
223 |
apply (rule_tac x="range A" in exI) |
|
224 |
apply auto |
|
225 |
done |
|
50883 | 226 |
|
51105 | 227 |
lemma (in first_countable_topology) first_countable_basis_Int_stableE: |
228 |
obtains A where "countable A" "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a" |
|
229 |
"\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)" |
|
230 |
"\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<inter> b \<in> A" |
|
231 |
proof atomize_elim |
|
55522 | 232 |
obtain A' where A': |
233 |
"countable A'" |
|
234 |
"\<And>a. a \<in> A' \<Longrightarrow> x \<in> a" |
|
235 |
"\<And>a. a \<in> A' \<Longrightarrow> open a" |
|
236 |
"\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>a\<in>A'. a \<subseteq> S" |
|
237 |
by (rule first_countable_basisE) blast |
|
51105 | 238 |
def A \<equiv> "(\<lambda>N. \<Inter>((\<lambda>n. from_nat_into A' n) ` N)) ` (Collect finite::nat set set)" |
53255 | 239 |
then show "\<exists>A. countable A \<and> (\<forall>a. a \<in> A \<longrightarrow> x \<in> a) \<and> (\<forall>a. a \<in> A \<longrightarrow> open a) \<and> |
51105 | 240 |
(\<forall>S. open S \<longrightarrow> x \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)) \<and> (\<forall>a b. a \<in> A \<longrightarrow> b \<in> A \<longrightarrow> a \<inter> b \<in> A)" |
241 |
proof (safe intro!: exI[where x=A]) |
|
53255 | 242 |
show "countable A" |
243 |
unfolding A_def by (intro countable_image countable_Collect_finite) |
|
244 |
fix a |
|
245 |
assume "a \<in> A" |
|
246 |
then show "x \<in> a" "open a" |
|
247 |
using A'(4)[OF open_UNIV] by (auto simp: A_def intro: A' from_nat_into) |
|
51105 | 248 |
next |
52141
eff000cab70f
weaker precendence of syntax for big intersection and union on sets
haftmann
parents:
51773
diff
changeset
|
249 |
let ?int = "\<lambda>N. \<Inter>(from_nat_into A' ` N)" |
53255 | 250 |
fix a b |
251 |
assume "a \<in> A" "b \<in> A" |
|
252 |
then obtain N M where "a = ?int N" "b = ?int M" "finite (N \<union> M)" |
|
253 |
by (auto simp: A_def) |
|
254 |
then show "a \<inter> b \<in> A" |
|
255 |
by (auto simp: A_def intro!: image_eqI[where x="N \<union> M"]) |
|
51105 | 256 |
next |
53255 | 257 |
fix S |
258 |
assume "open S" "x \<in> S" |
|
259 |
then obtain a where a: "a\<in>A'" "a \<subseteq> S" using A' by blast |
|
260 |
then show "\<exists>a\<in>A. a \<subseteq> S" using a A' |
|
51105 | 261 |
by (intro bexI[where x=a]) (auto simp: A_def intro: image_eqI[where x="{to_nat_on A' a}"]) |
262 |
qed |
|
263 |
qed |
|
264 |
||
51473 | 265 |
lemma (in topological_space) first_countableI: |
53255 | 266 |
assumes "countable A" |
267 |
and 1: "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a" |
|
268 |
and 2: "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>a\<in>A. a \<subseteq> S" |
|
51473 | 269 |
shows "\<exists>A::nat \<Rightarrow> 'a set. (\<forall>i. x \<in> A i \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))" |
270 |
proof (safe intro!: exI[of _ "from_nat_into A"]) |
|
53255 | 271 |
fix i |
51473 | 272 |
have "A \<noteq> {}" using 2[of UNIV] by auto |
53255 | 273 |
show "x \<in> from_nat_into A i" "open (from_nat_into A i)" |
274 |
using range_from_nat_into_subset[OF `A \<noteq> {}`] 1 by auto |
|
275 |
next |
|
276 |
fix S |
|
277 |
assume "open S" "x\<in>S" from 2[OF this] |
|
278 |
show "\<exists>i. from_nat_into A i \<subseteq> S" |
|
279 |
using subset_range_from_nat_into[OF `countable A`] by auto |
|
51473 | 280 |
qed |
51350 | 281 |
|
50883 | 282 |
instance prod :: (first_countable_topology, first_countable_topology) first_countable_topology |
283 |
proof |
|
284 |
fix x :: "'a \<times> 'b" |
|
55522 | 285 |
obtain A where A: |
286 |
"countable A" |
|
287 |
"\<And>a. a \<in> A \<Longrightarrow> fst x \<in> a" |
|
288 |
"\<And>a. a \<in> A \<Longrightarrow> open a" |
|
289 |
"\<And>S. open S \<Longrightarrow> fst x \<in> S \<Longrightarrow> \<exists>a\<in>A. a \<subseteq> S" |
|
290 |
by (rule first_countable_basisE[of "fst x"]) blast |
|
291 |
obtain B where B: |
|
292 |
"countable B" |
|
293 |
"\<And>a. a \<in> B \<Longrightarrow> snd x \<in> a" |
|
294 |
"\<And>a. a \<in> B \<Longrightarrow> open a" |
|
295 |
"\<And>S. open S \<Longrightarrow> snd x \<in> S \<Longrightarrow> \<exists>a\<in>B. a \<subseteq> S" |
|
296 |
by (rule first_countable_basisE[of "snd x"]) blast |
|
53282 | 297 |
show "\<exists>A::nat \<Rightarrow> ('a \<times> 'b) set. |
298 |
(\<forall>i. x \<in> A i \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))" |
|
51473 | 299 |
proof (rule first_countableI[of "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"], safe) |
53255 | 300 |
fix a b |
301 |
assume x: "a \<in> A" "b \<in> B" |
|
53640 | 302 |
with A(2, 3)[of a] B(2, 3)[of b] show "x \<in> a \<times> b" and "open (a \<times> b)" |
303 |
unfolding mem_Times_iff |
|
304 |
by (auto intro: open_Times) |
|
50883 | 305 |
next |
53255 | 306 |
fix S |
307 |
assume "open S" "x \<in> S" |
|
55522 | 308 |
then obtain a' b' where a'b': "open a'" "open b'" "x \<in> a' \<times> b'" "a' \<times> b' \<subseteq> S" |
309 |
by (rule open_prod_elim) |
|
310 |
moreover |
|
311 |
from a'b' A(4)[of a'] B(4)[of b'] |
|
312 |
obtain a b where "a \<in> A" "a \<subseteq> a'" "b \<in> B" "b \<subseteq> b'" |
|
313 |
by auto |
|
314 |
ultimately |
|
315 |
show "\<exists>a\<in>(\<lambda>(a, b). a \<times> b) ` (A \<times> B). a \<subseteq> S" |
|
50883 | 316 |
by (auto intro!: bexI[of _ "a \<times> b"] bexI[of _ a] bexI[of _ b]) |
317 |
qed (simp add: A B) |
|
318 |
qed |
|
319 |
||
50881
ae630bab13da
renamed countable_basis_space to second_countable_topology
hoelzl
parents:
50526
diff
changeset
|
320 |
class second_countable_topology = topological_space + |
53282 | 321 |
assumes ex_countable_subbasis: |
322 |
"\<exists>B::'a::topological_space set set. countable B \<and> open = generate_topology B" |
|
51343
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
323 |
begin |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
324 |
|
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
325 |
lemma ex_countable_basis: "\<exists>B::'a set set. countable B \<and> topological_basis B" |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
326 |
proof - |
53255 | 327 |
from ex_countable_subbasis obtain B where B: "countable B" "open = generate_topology B" |
328 |
by blast |
|
51343
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
329 |
let ?B = "Inter ` {b. finite b \<and> b \<subseteq> B }" |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
330 |
|
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
331 |
show ?thesis |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
332 |
proof (intro exI conjI) |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
333 |
show "countable ?B" |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
334 |
by (intro countable_image countable_Collect_finite_subset B) |
53255 | 335 |
{ |
336 |
fix S |
|
337 |
assume "open S" |
|
51343
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
338 |
then have "\<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. (\<Union>b\<in>B'. \<Inter>b) = S" |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
339 |
unfolding B |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
340 |
proof induct |
53255 | 341 |
case UNIV |
342 |
show ?case by (intro exI[of _ "{{}}"]) simp |
|
51343
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
343 |
next |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
344 |
case (Int a b) |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
345 |
then obtain x y where x: "a = UNION x Inter" "\<And>i. i \<in> x \<Longrightarrow> finite i \<and> i \<subseteq> B" |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
346 |
and y: "b = UNION y Inter" "\<And>i. i \<in> y \<Longrightarrow> finite i \<and> i \<subseteq> B" |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
347 |
by blast |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
348 |
show ?case |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
349 |
unfolding x y Int_UN_distrib2 |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
350 |
by (intro exI[of _ "{i \<union> j| i j. i \<in> x \<and> j \<in> y}"]) (auto dest: x(2) y(2)) |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
351 |
next |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
352 |
case (UN K) |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
353 |
then have "\<forall>k\<in>K. \<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. UNION B' Inter = k" by auto |
55522 | 354 |
then obtain k where |
355 |
"\<forall>ka\<in>K. k ka \<subseteq> {b. finite b \<and> b \<subseteq> B} \<and> UNION (k ka) Inter = ka" |
|
356 |
unfolding bchoice_iff .. |
|
51343
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
357 |
then show "\<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. UNION B' Inter = \<Union>K" |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
358 |
by (intro exI[of _ "UNION K k"]) auto |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
359 |
next |
53255 | 360 |
case (Basis S) |
361 |
then show ?case |
|
51343
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
362 |
by (intro exI[of _ "{{S}}"]) auto |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
363 |
qed |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
364 |
then have "(\<exists>B'\<subseteq>Inter ` {b. finite b \<and> b \<subseteq> B}. \<Union>B' = S)" |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
365 |
unfolding subset_image_iff by blast } |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
366 |
then show "topological_basis ?B" |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
367 |
unfolding topological_space_class.topological_basis_def |
53282 | 368 |
by (safe intro!: topological_space_class.open_Inter) |
51343
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
369 |
(simp_all add: B generate_topology.Basis subset_eq) |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
370 |
qed |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
371 |
qed |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
372 |
|
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
373 |
end |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
374 |
|
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
375 |
sublocale second_countable_topology < |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
376 |
countable_basis "SOME B. countable B \<and> topological_basis B" |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
377 |
using someI_ex[OF ex_countable_basis] |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
378 |
by unfold_locales safe |
50094
84ddcf5364b4
allow arbitrary enumerations of basis in locale for generation of borel sets
immler
parents:
50087
diff
changeset
|
379 |
|
50882
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset
|
380 |
instance prod :: (second_countable_topology, second_countable_topology) second_countable_topology |
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset
|
381 |
proof |
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset
|
382 |
obtain A :: "'a set set" where "countable A" "topological_basis A" |
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset
|
383 |
using ex_countable_basis by auto |
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset
|
384 |
moreover |
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset
|
385 |
obtain B :: "'b set set" where "countable B" "topological_basis B" |
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset
|
386 |
using ex_countable_basis by auto |
51343
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
387 |
ultimately show "\<exists>B::('a \<times> 'b) set set. countable B \<and> open = generate_topology B" |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
388 |
by (auto intro!: exI[of _ "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"] topological_basis_prod |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
389 |
topological_basis_imp_subbasis) |
50882
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset
|
390 |
qed |
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset
|
391 |
|
50883 | 392 |
instance second_countable_topology \<subseteq> first_countable_topology |
393 |
proof |
|
394 |
fix x :: 'a |
|
395 |
def B \<equiv> "SOME B::'a set set. countable B \<and> topological_basis B" |
|
396 |
then have B: "countable B" "topological_basis B" |
|
397 |
using countable_basis is_basis |
|
398 |
by (auto simp: countable_basis is_basis) |
|
53282 | 399 |
then show "\<exists>A::nat \<Rightarrow> 'a set. |
400 |
(\<forall>i. x \<in> A i \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))" |
|
51473 | 401 |
by (intro first_countableI[of "{b\<in>B. x \<in> b}"]) |
402 |
(fastforce simp: topological_space_class.topological_basis_def)+ |
|
50883 | 403 |
qed |
404 |
||
53255 | 405 |
|
50087 | 406 |
subsection {* Polish spaces *} |
407 |
||
408 |
text {* Textbooks define Polish spaces as completely metrizable. |
|
409 |
We assume the topology to be complete for a given metric. *} |
|
410 |
||
50881
ae630bab13da
renamed countable_basis_space to second_countable_topology
hoelzl
parents:
50526
diff
changeset
|
411 |
class polish_space = complete_space + second_countable_topology |
50087 | 412 |
|
44517 | 413 |
subsection {* General notion of a topology as a value *} |
33175 | 414 |
|
53255 | 415 |
definition "istopology L \<longleftrightarrow> |
416 |
L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union> K))" |
|
417 |
||
49834 | 418 |
typedef 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}" |
33175 | 419 |
morphisms "openin" "topology" |
420 |
unfolding istopology_def by blast |
|
421 |
||
422 |
lemma istopology_open_in[intro]: "istopology(openin U)" |
|
423 |
using openin[of U] by blast |
|
424 |
||
425 |
lemma topology_inverse': "istopology U \<Longrightarrow> openin (topology U) = U" |
|
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset
|
426 |
using topology_inverse[unfolded mem_Collect_eq] . |
33175 | 427 |
|
428 |
lemma topology_inverse_iff: "istopology U \<longleftrightarrow> openin (topology U) = U" |
|
429 |
using topology_inverse[of U] istopology_open_in[of "topology U"] by auto |
|
430 |
||
431 |
lemma topology_eq: "T1 = T2 \<longleftrightarrow> (\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S)" |
|
53255 | 432 |
proof |
433 |
assume "T1 = T2" |
|
434 |
then show "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S" by simp |
|
435 |
next |
|
436 |
assume H: "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S" |
|
437 |
then have "openin T1 = openin T2" by (simp add: fun_eq_iff) |
|
438 |
then have "topology (openin T1) = topology (openin T2)" by simp |
|
439 |
then show "T1 = T2" unfolding openin_inverse . |
|
33175 | 440 |
qed |
441 |
||
442 |
text{* Infer the "universe" from union of all sets in the topology. *} |
|
443 |
||
53640 | 444 |
definition "topspace T = \<Union>{S. openin T S}" |
33175 | 445 |
|
44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
446 |
subsubsection {* Main properties of open sets *} |
33175 | 447 |
|
448 |
lemma openin_clauses: |
|
449 |
fixes U :: "'a topology" |
|
53282 | 450 |
shows |
451 |
"openin U {}" |
|
452 |
"\<And>S T. openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S\<inter>T)" |
|
453 |
"\<And>K. (\<forall>S \<in> K. openin U S) \<Longrightarrow> openin U (\<Union>K)" |
|
454 |
using openin[of U] unfolding istopology_def mem_Collect_eq by fast+ |
|
33175 | 455 |
|
456 |
lemma openin_subset[intro]: "openin U S \<Longrightarrow> S \<subseteq> topspace U" |
|
457 |
unfolding topspace_def by blast |
|
53255 | 458 |
|
459 |
lemma openin_empty[simp]: "openin U {}" |
|
460 |
by (simp add: openin_clauses) |
|
33175 | 461 |
|
462 |
lemma openin_Int[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<inter> T)" |
|
36362
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
36360
diff
changeset
|
463 |
using openin_clauses by simp |
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
36360
diff
changeset
|
464 |
|
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
36360
diff
changeset
|
465 |
lemma openin_Union[intro]: "(\<forall>S \<in>K. openin U S) \<Longrightarrow> openin U (\<Union> K)" |
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
36360
diff
changeset
|
466 |
using openin_clauses by simp |
33175 | 467 |
|
468 |
lemma openin_Un[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<union> T)" |
|
469 |
using openin_Union[of "{S,T}" U] by auto |
|
470 |
||
53255 | 471 |
lemma openin_topspace[intro, simp]: "openin U (topspace U)" |
472 |
by (simp add: openin_Union topspace_def) |
|
33175 | 473 |
|
49711 | 474 |
lemma openin_subopen: "openin U S \<longleftrightarrow> (\<forall>x \<in> S. \<exists>T. openin U T \<and> x \<in> T \<and> T \<subseteq> S)" |
475 |
(is "?lhs \<longleftrightarrow> ?rhs") |
|
36584 | 476 |
proof |
49711 | 477 |
assume ?lhs |
478 |
then show ?rhs by auto |
|
36584 | 479 |
next |
480 |
assume H: ?rhs |
|
481 |
let ?t = "\<Union>{T. openin U T \<and> T \<subseteq> S}" |
|
482 |
have "openin U ?t" by (simp add: openin_Union) |
|
483 |
also have "?t = S" using H by auto |
|
484 |
finally show "openin U S" . |
|
33175 | 485 |
qed |
486 |
||
49711 | 487 |
|
44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
488 |
subsubsection {* Closed sets *} |
33175 | 489 |
|
490 |
definition "closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U - S)" |
|
491 |
||
53255 | 492 |
lemma closedin_subset: "closedin U S \<Longrightarrow> S \<subseteq> topspace U" |
493 |
by (metis closedin_def) |
|
494 |
||
495 |
lemma closedin_empty[simp]: "closedin U {}" |
|
496 |
by (simp add: closedin_def) |
|
497 |
||
498 |
lemma closedin_topspace[intro, simp]: "closedin U (topspace U)" |
|
499 |
by (simp add: closedin_def) |
|
500 |
||
33175 | 501 |
lemma closedin_Un[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<union> T)" |
502 |
by (auto simp add: Diff_Un closedin_def) |
|
503 |
||
53255 | 504 |
lemma Diff_Inter[intro]: "A - \<Inter>S = \<Union> {A - s|s. s\<in>S}" |
505 |
by auto |
|
506 |
||
507 |
lemma closedin_Inter[intro]: |
|
508 |
assumes Ke: "K \<noteq> {}" |
|
509 |
and Kc: "\<forall>S \<in>K. closedin U S" |
|
510 |
shows "closedin U (\<Inter> K)" |
|
511 |
using Ke Kc unfolding closedin_def Diff_Inter by auto |
|
33175 | 512 |
|
513 |
lemma closedin_Int[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<inter> T)" |
|
514 |
using closedin_Inter[of "{S,T}" U] by auto |
|
515 |
||
53255 | 516 |
lemma Diff_Diff_Int: "A - (A - B) = A \<inter> B" |
517 |
by blast |
|
518 |
||
33175 | 519 |
lemma openin_closedin_eq: "openin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> closedin U (topspace U - S)" |
520 |
apply (auto simp add: closedin_def Diff_Diff_Int inf_absorb2) |
|
521 |
apply (metis openin_subset subset_eq) |
|
522 |
done |
|
523 |
||
53255 | 524 |
lemma openin_closedin: "S \<subseteq> topspace U \<Longrightarrow> (openin U S \<longleftrightarrow> closedin U (topspace U - S))" |
33175 | 525 |
by (simp add: openin_closedin_eq) |
526 |
||
53255 | 527 |
lemma openin_diff[intro]: |
528 |
assumes oS: "openin U S" |
|
529 |
and cT: "closedin U T" |
|
530 |
shows "openin U (S - T)" |
|
531 |
proof - |
|
33175 | 532 |
have "S - T = S \<inter> (topspace U - T)" using openin_subset[of U S] oS cT |
533 |
by (auto simp add: topspace_def openin_subset) |
|
53282 | 534 |
then show ?thesis using oS cT |
535 |
by (auto simp add: closedin_def) |
|
33175 | 536 |
qed |
537 |
||
53255 | 538 |
lemma closedin_diff[intro]: |
539 |
assumes oS: "closedin U S" |
|
540 |
and cT: "openin U T" |
|
541 |
shows "closedin U (S - T)" |
|
542 |
proof - |
|
543 |
have "S - T = S \<inter> (topspace U - T)" |
|
53282 | 544 |
using closedin_subset[of U S] oS cT by (auto simp add: topspace_def) |
53255 | 545 |
then show ?thesis |
546 |
using oS cT by (auto simp add: openin_closedin_eq) |
|
547 |
qed |
|
548 |
||
33175 | 549 |
|
44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
550 |
subsubsection {* Subspace topology *} |
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset
|
551 |
|
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset
|
552 |
definition "subtopology U V = topology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)" |
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset
|
553 |
|
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset
|
554 |
lemma istopology_subtopology: "istopology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)" |
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset
|
555 |
(is "istopology ?L") |
53255 | 556 |
proof - |
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset
|
557 |
have "?L {}" by blast |
53255 | 558 |
{ |
559 |
fix A B |
|
560 |
assume A: "?L A" and B: "?L B" |
|
561 |
from A B obtain Sa and Sb where Sa: "openin U Sa" "A = Sa \<inter> V" and Sb: "openin U Sb" "B = Sb \<inter> V" |
|
562 |
by blast |
|
563 |
have "A \<inter> B = (Sa \<inter> Sb) \<inter> V" "openin U (Sa \<inter> Sb)" |
|
564 |
using Sa Sb by blast+ |
|
565 |
then have "?L (A \<inter> B)" by blast |
|
566 |
} |
|
33175 | 567 |
moreover |
53255 | 568 |
{ |
53282 | 569 |
fix K |
570 |
assume K: "K \<subseteq> Collect ?L" |
|
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset
|
571 |
have th0: "Collect ?L = (\<lambda>S. S \<inter> V) ` Collect (openin U)" |
55775 | 572 |
by blast |
33175 | 573 |
from K[unfolded th0 subset_image_iff] |
53255 | 574 |
obtain Sk where Sk: "Sk \<subseteq> Collect (openin U)" "K = (\<lambda>S. S \<inter> V) ` Sk" |
575 |
by blast |
|
576 |
have "\<Union>K = (\<Union>Sk) \<inter> V" |
|
577 |
using Sk by auto |
|
578 |
moreover have "openin U (\<Union> Sk)" |
|
579 |
using Sk by (auto simp add: subset_eq) |
|
580 |
ultimately have "?L (\<Union>K)" by blast |
|
581 |
} |
|
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset
|
582 |
ultimately show ?thesis |
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset
|
583 |
unfolding subset_eq mem_Collect_eq istopology_def by blast |
33175 | 584 |
qed |
585 |
||
53255 | 586 |
lemma openin_subtopology: "openin (subtopology U V) S \<longleftrightarrow> (\<exists>T. openin U T \<and> S = T \<inter> V)" |
33175 | 587 |
unfolding subtopology_def topology_inverse'[OF istopology_subtopology] |
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset
|
588 |
by auto |
33175 | 589 |
|
53255 | 590 |
lemma topspace_subtopology: "topspace (subtopology U V) = topspace U \<inter> V" |
33175 | 591 |
by (auto simp add: topspace_def openin_subtopology) |
592 |
||
53255 | 593 |
lemma closedin_subtopology: "closedin (subtopology U V) S \<longleftrightarrow> (\<exists>T. closedin U T \<and> S = T \<inter> V)" |
33175 | 594 |
unfolding closedin_def topspace_subtopology |
55775 | 595 |
by (auto simp add: openin_subtopology) |
33175 | 596 |
|
597 |
lemma openin_subtopology_refl: "openin (subtopology U V) V \<longleftrightarrow> V \<subseteq> topspace U" |
|
598 |
unfolding openin_subtopology |
|
55775 | 599 |
by auto (metis IntD1 in_mono openin_subset) |
49711 | 600 |
|
601 |
lemma subtopology_superset: |
|
602 |
assumes UV: "topspace U \<subseteq> V" |
|
33175 | 603 |
shows "subtopology U V = U" |
53255 | 604 |
proof - |
605 |
{ |
|
606 |
fix S |
|
607 |
{ |
|
608 |
fix T |
|
609 |
assume T: "openin U T" "S = T \<inter> V" |
|
610 |
from T openin_subset[OF T(1)] UV have eq: "S = T" |
|
611 |
by blast |
|
612 |
have "openin U S" |
|
613 |
unfolding eq using T by blast |
|
614 |
} |
|
33175 | 615 |
moreover |
53255 | 616 |
{ |
617 |
assume S: "openin U S" |
|
618 |
then have "\<exists>T. openin U T \<and> S = T \<inter> V" |
|
619 |
using openin_subset[OF S] UV by auto |
|
620 |
} |
|
621 |
ultimately have "(\<exists>T. openin U T \<and> S = T \<inter> V) \<longleftrightarrow> openin U S" |
|
622 |
by blast |
|
623 |
} |
|
624 |
then show ?thesis |
|
625 |
unfolding topology_eq openin_subtopology by blast |
|
33175 | 626 |
qed |
627 |
||
628 |
lemma subtopology_topspace[simp]: "subtopology U (topspace U) = U" |
|
629 |
by (simp add: subtopology_superset) |
|
630 |
||
631 |
lemma subtopology_UNIV[simp]: "subtopology U UNIV = U" |
|
632 |
by (simp add: subtopology_superset) |
|
633 |
||
53255 | 634 |
|
44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
635 |
subsubsection {* The standard Euclidean topology *} |
33175 | 636 |
|
53255 | 637 |
definition euclidean :: "'a::topological_space topology" |
638 |
where "euclidean = topology open" |
|
33175 | 639 |
|
640 |
lemma open_openin: "open S \<longleftrightarrow> openin euclidean S" |
|
641 |
unfolding euclidean_def |
|
642 |
apply (rule cong[where x=S and y=S]) |
|
643 |
apply (rule topology_inverse[symmetric]) |
|
644 |
apply (auto simp add: istopology_def) |
|
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset
|
645 |
done |
33175 | 646 |
|
647 |
lemma topspace_euclidean: "topspace euclidean = UNIV" |
|
648 |
apply (simp add: topspace_def) |
|
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39198
diff
changeset
|
649 |
apply (rule set_eqI) |
53255 | 650 |
apply (auto simp add: open_openin[symmetric]) |
651 |
done |
|
33175 | 652 |
|
653 |
lemma topspace_euclidean_subtopology[simp]: "topspace (subtopology euclidean S) = S" |
|
654 |
by (simp add: topspace_euclidean topspace_subtopology) |
|
655 |
||
656 |
lemma closed_closedin: "closed S \<longleftrightarrow> closedin euclidean S" |
|
657 |
by (simp add: closed_def closedin_def topspace_euclidean open_openin Compl_eq_Diff_UNIV) |
|
658 |
||
659 |
lemma open_subopen: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S)" |
|
660 |
by (simp add: open_openin openin_subopen[symmetric]) |
|
661 |
||
44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
662 |
text {* Basic "localization" results are handy for connectedness. *} |
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
663 |
|
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
664 |
lemma openin_open: "openin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. open T \<and> (S = U \<inter> T))" |
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
665 |
by (auto simp add: openin_subtopology open_openin[symmetric]) |
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
666 |
|
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
667 |
lemma openin_open_Int[intro]: "open S \<Longrightarrow> openin (subtopology euclidean U) (U \<inter> S)" |
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
668 |
by (auto simp add: openin_open) |
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
669 |
|
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
670 |
lemma open_openin_trans[trans]: |
53255 | 671 |
"open S \<Longrightarrow> open T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> openin (subtopology euclidean S) T" |
44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
672 |
by (metis Int_absorb1 openin_open_Int) |
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
673 |
|
53255 | 674 |
lemma open_subset: "S \<subseteq> T \<Longrightarrow> open S \<Longrightarrow> openin (subtopology euclidean T) S" |
44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
675 |
by (auto simp add: openin_open) |
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
676 |
|
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
677 |
lemma closedin_closed: "closedin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. closed T \<and> S = U \<inter> T)" |
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
678 |
by (simp add: closedin_subtopology closed_closedin Int_ac) |
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
679 |
|
53291 | 680 |
lemma closedin_closed_Int: "closed S \<Longrightarrow> closedin (subtopology euclidean U) (U \<inter> S)" |
44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
681 |
by (metis closedin_closed) |
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
682 |
|
53282 | 683 |
lemma closed_closedin_trans: |
684 |
"closed S \<Longrightarrow> closed T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> closedin (subtopology euclidean S) T" |
|
55775 | 685 |
by (metis closedin_closed inf.absorb2) |
44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
686 |
|
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
687 |
lemma closed_subset: "S \<subseteq> T \<Longrightarrow> closed S \<Longrightarrow> closedin (subtopology euclidean T) S" |
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
688 |
by (auto simp add: closedin_closed) |
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
689 |
|
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
690 |
lemma openin_euclidean_subtopology_iff: |
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
691 |
fixes S U :: "'a::metric_space set" |
53255 | 692 |
shows "openin (subtopology euclidean U) S \<longleftrightarrow> |
693 |
S \<subseteq> U \<and> (\<forall>x\<in>S. \<exists>e>0. \<forall>x'\<in>U. dist x' x < e \<longrightarrow> x'\<in> S)" |
|
694 |
(is "?lhs \<longleftrightarrow> ?rhs") |
|
44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
695 |
proof |
53255 | 696 |
assume ?lhs |
53282 | 697 |
then show ?rhs |
698 |
unfolding openin_open open_dist by blast |
|
44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
699 |
next |
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
700 |
def T \<equiv> "{x. \<exists>a\<in>S. \<exists>d>0. (\<forall>y\<in>U. dist y a < d \<longrightarrow> y \<in> S) \<and> dist x a < d}" |
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
701 |
have 1: "\<forall>x\<in>T. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> T" |
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
702 |
unfolding T_def |
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
703 |
apply clarsimp |
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
704 |
apply (rule_tac x="d - dist x a" in exI) |
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
705 |
apply (clarsimp simp add: less_diff_eq) |
55775 | 706 |
by (metis dist_commute dist_triangle_lt) |
53282 | 707 |
assume ?rhs then have 2: "S = U \<inter> T" |
55775 | 708 |
unfolding T_def |
709 |
by auto (metis dist_self) |
|
44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
710 |
from 1 2 show ?lhs |
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
711 |
unfolding openin_open open_dist by fast |
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
712 |
qed |
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
713 |
|
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
714 |
text {* These "transitivity" results are handy too *} |
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
715 |
|
53255 | 716 |
lemma openin_trans[trans]: |
717 |
"openin (subtopology euclidean T) S \<Longrightarrow> openin (subtopology euclidean U) T \<Longrightarrow> |
|
718 |
openin (subtopology euclidean U) S" |
|
44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
719 |
unfolding open_openin openin_open by blast |
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
720 |
|
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
721 |
lemma openin_open_trans: "openin (subtopology euclidean T) S \<Longrightarrow> open T \<Longrightarrow> open S" |
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
722 |
by (auto simp add: openin_open intro: openin_trans) |
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
723 |
|
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
724 |
lemma closedin_trans[trans]: |
53255 | 725 |
"closedin (subtopology euclidean T) S \<Longrightarrow> closedin (subtopology euclidean U) T \<Longrightarrow> |
726 |
closedin (subtopology euclidean U) S" |
|
44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
727 |
by (auto simp add: closedin_closed closed_closedin closed_Inter Int_assoc) |
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
728 |
|
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
729 |
lemma closedin_closed_trans: "closedin (subtopology euclidean T) S \<Longrightarrow> closed T \<Longrightarrow> closed S" |
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
730 |
by (auto simp add: closedin_closed intro: closedin_trans) |
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
731 |
|
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
732 |
|
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
733 |
subsection {* Open and closed balls *} |
33175 | 734 |
|
53255 | 735 |
definition ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" |
736 |
where "ball x e = {y. dist x y < e}" |
|
737 |
||
738 |
definition cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" |
|
739 |
where "cball x e = {y. dist x y \<le> e}" |
|
33175 | 740 |
|
45776
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset
|
741 |
lemma mem_ball [simp]: "y \<in> ball x e \<longleftrightarrow> dist x y < e" |
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset
|
742 |
by (simp add: ball_def) |
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset
|
743 |
|
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset
|
744 |
lemma mem_cball [simp]: "y \<in> cball x e \<longleftrightarrow> dist x y \<le> e" |
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset
|
745 |
by (simp add: cball_def) |
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset
|
746 |
|
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset
|
747 |
lemma mem_ball_0: |
33175 | 748 |
fixes x :: "'a::real_normed_vector" |
749 |
shows "x \<in> ball 0 e \<longleftrightarrow> norm x < e" |
|
750 |
by (simp add: dist_norm) |
|
751 |
||
45776
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset
|
752 |
lemma mem_cball_0: |
33175 | 753 |
fixes x :: "'a::real_normed_vector" |
754 |
shows "x \<in> cball 0 e \<longleftrightarrow> norm x \<le> e" |
|
755 |
by (simp add: dist_norm) |
|
756 |
||
45776
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset
|
757 |
lemma centre_in_ball: "x \<in> ball x e \<longleftrightarrow> 0 < e" |
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset
|
758 |
by simp |
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset
|
759 |
|
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset
|
760 |
lemma centre_in_cball: "x \<in> cball x e \<longleftrightarrow> 0 \<le> e" |
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset
|
761 |
by simp |
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset
|
762 |
|
53255 | 763 |
lemma ball_subset_cball[simp,intro]: "ball x e \<subseteq> cball x e" |
764 |
by (simp add: subset_eq) |
|
765 |
||
53282 | 766 |
lemma subset_ball[intro]: "d \<le> e \<Longrightarrow> ball x d \<subseteq> ball x e" |
53255 | 767 |
by (simp add: subset_eq) |
768 |
||
53282 | 769 |
lemma subset_cball[intro]: "d \<le> e \<Longrightarrow> cball x d \<subseteq> cball x e" |
53255 | 770 |
by (simp add: subset_eq) |
771 |
||
33175 | 772 |
lemma ball_max_Un: "ball a (max r s) = ball a r \<union> ball a s" |
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39198
diff
changeset
|
773 |
by (simp add: set_eq_iff) arith |
33175 | 774 |
|
775 |
lemma ball_min_Int: "ball a (min r s) = ball a r \<inter> ball a s" |
|
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39198
diff
changeset
|
776 |
by (simp add: set_eq_iff) |
33175 | 777 |
|
53255 | 778 |
lemma diff_less_iff: |
779 |
"(a::real) - b > 0 \<longleftrightarrow> a > b" |
|
33175 | 780 |
"(a::real) - b < 0 \<longleftrightarrow> a < b" |
53255 | 781 |
"a - b < c \<longleftrightarrow> a < c + b" "a - b > c \<longleftrightarrow> a > c + b" |
782 |
by arith+ |
|
783 |
||
784 |
lemma diff_le_iff: |
|
785 |
"(a::real) - b \<ge> 0 \<longleftrightarrow> a \<ge> b" |
|
786 |
"(a::real) - b \<le> 0 \<longleftrightarrow> a \<le> b" |
|
787 |
"a - b \<le> c \<longleftrightarrow> a \<le> c + b" |
|
788 |
"a - b \<ge> c \<longleftrightarrow> a \<ge> c + b" |
|
789 |
by arith+ |
|
33175 | 790 |
|
54070 | 791 |
lemma open_ball [intro, simp]: "open (ball x e)" |
792 |
proof - |
|
793 |
have "open (dist x -` {..<e})" |
|
794 |
by (intro open_vimage open_lessThan continuous_on_intros) |
|
795 |
also have "dist x -` {..<e} = ball x e" |
|
796 |
by auto |
|
797 |
finally show ?thesis . |
|
798 |
qed |
|
33175 | 799 |
|
800 |
lemma open_contains_ball: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. ball x e \<subseteq> S)" |
|
801 |
unfolding open_dist subset_eq mem_ball Ball_def dist_commute .. |
|
802 |
||
33714
eb2574ac4173
Added new lemmas to Euclidean Space by Robert Himmelmann
hoelzl
parents:
33324
diff
changeset
|
803 |
lemma openE[elim?]: |
53282 | 804 |
assumes "open S" "x\<in>S" |
33714
eb2574ac4173
Added new lemmas to Euclidean Space by Robert Himmelmann
hoelzl
parents:
33324
diff
changeset
|
805 |
obtains e where "e>0" "ball x e \<subseteq> S" |
eb2574ac4173
Added new lemmas to Euclidean Space by Robert Himmelmann
hoelzl
parents:
33324
diff
changeset
|
806 |
using assms unfolding open_contains_ball by auto |
eb2574ac4173
Added new lemmas to Euclidean Space by Robert Himmelmann
hoelzl
parents:
33324
diff
changeset
|
807 |
|
33175 | 808 |
lemma open_contains_ball_eq: "open S \<Longrightarrow> \<forall>x. x\<in>S \<longleftrightarrow> (\<exists>e>0. ball x e \<subseteq> S)" |
809 |
by (metis open_contains_ball subset_eq centre_in_ball) |
|
810 |
||
811 |
lemma ball_eq_empty[simp]: "ball x e = {} \<longleftrightarrow> e \<le> 0" |
|
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39198
diff
changeset
|
812 |
unfolding mem_ball set_eq_iff |
33175 | 813 |
apply (simp add: not_less) |
52624 | 814 |
apply (metis zero_le_dist order_trans dist_self) |
815 |
done |
|
33175 | 816 |
|
53291 | 817 |
lemma ball_empty[intro]: "e \<le> 0 \<Longrightarrow> ball x e = {}" by simp |
33175 | 818 |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
819 |
lemma euclidean_dist_l2: |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
820 |
fixes x y :: "'a :: euclidean_space" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
821 |
shows "dist x y = setL2 (\<lambda>i. dist (x \<bullet> i) (y \<bullet> i)) Basis" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
822 |
unfolding dist_norm norm_eq_sqrt_inner setL2_def |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
823 |
by (subst euclidean_inner) (simp add: power2_eq_square inner_diff_left) |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
824 |
|
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
825 |
definition (in euclidean_space) eucl_less (infix "<e" 50) |
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
826 |
where "eucl_less a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i)" |
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
827 |
|
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
828 |
definition box_eucl_less: "box a b = {x. a <e x \<and> x <e b}" |
56188 | 829 |
definition "cbox a b = {x. \<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i}" |
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
830 |
|
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
831 |
lemma box_def: "box a b = {x. \<forall>i\<in>Basis. a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i}" |
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
832 |
and in_box_eucl_less: "x \<in> box a b \<longleftrightarrow> a <e x \<and> x <e b" |
56188 | 833 |
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)" |
834 |
"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)" |
|
835 |
by (auto simp: box_eucl_less eucl_less_def cbox_def) |
|
836 |
||
837 |
lemma mem_box_real[simp]: |
|
838 |
"(x::real) \<in> box a b \<longleftrightarrow> a < x \<and> x < b" |
|
839 |
"(x::real) \<in> cbox a b \<longleftrightarrow> a \<le> x \<and> x \<le> b" |
|
840 |
by (auto simp: mem_box) |
|
841 |
||
842 |
lemma box_real[simp]: |
|
843 |
fixes a b:: real |
|
844 |
shows "box a b = {a <..< b}" "cbox a b = {a .. b}" |
|
845 |
by auto |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
846 |
|
50087 | 847 |
lemma rational_boxes: |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
848 |
fixes x :: "'a\<Colon>euclidean_space" |
53291 | 849 |
assumes "e > 0" |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
850 |
shows "\<exists>a b. (\<forall>i\<in>Basis. a \<bullet> i \<in> \<rat> \<and> b \<bullet> i \<in> \<rat> ) \<and> x \<in> box a b \<and> box a b \<subseteq> ball x e" |
50087 | 851 |
proof - |
852 |
def e' \<equiv> "e / (2 * sqrt (real (DIM ('a))))" |
|
53291 | 853 |
then have e: "e' > 0" |
53255 | 854 |
using assms by (auto intro!: divide_pos_pos simp: DIM_positive) |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
855 |
have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x \<bullet> i \<and> x \<bullet> i - y < e'" (is "\<forall>i. ?th i") |
50087 | 856 |
proof |
53255 | 857 |
fix i |
858 |
from Rats_dense_in_real[of "x \<bullet> i - e'" "x \<bullet> i"] e |
|
859 |
show "?th i" by auto |
|
50087 | 860 |
qed |
55522 | 861 |
from choice[OF this] obtain a where |
862 |
a: "\<forall>xa. a xa \<in> \<rat> \<and> a xa < x \<bullet> xa \<and> x \<bullet> xa - a xa < e'" .. |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
863 |
have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x \<bullet> i < y \<and> y - x \<bullet> i < e'" (is "\<forall>i. ?th i") |
50087 | 864 |
proof |
53255 | 865 |
fix i |
866 |
from Rats_dense_in_real[of "x \<bullet> i" "x \<bullet> i + e'"] e |
|
867 |
show "?th i" by auto |
|
50087 | 868 |
qed |
55522 | 869 |
from choice[OF this] obtain b where |
870 |
b: "\<forall>xa. b xa \<in> \<rat> \<and> x \<bullet> xa < b xa \<and> b xa - x \<bullet> xa < e'" .. |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
871 |
let ?a = "\<Sum>i\<in>Basis. a i *\<^sub>R i" and ?b = "\<Sum>i\<in>Basis. b i *\<^sub>R i" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
872 |
show ?thesis |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
873 |
proof (rule exI[of _ ?a], rule exI[of _ ?b], safe) |
53255 | 874 |
fix y :: 'a |
875 |
assume *: "y \<in> box ?a ?b" |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52625
diff
changeset
|
876 |
have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)" |
50087 | 877 |
unfolding setL2_def[symmetric] by (rule euclidean_dist_l2) |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
878 |
also have "\<dots> < sqrt (\<Sum>(i::'a)\<in>Basis. e^2 / real (DIM('a)))" |
50087 | 879 |
proof (rule real_sqrt_less_mono, rule setsum_strict_mono) |
53255 | 880 |
fix i :: "'a" |
881 |
assume i: "i \<in> Basis" |
|
882 |
have "a i < y\<bullet>i \<and> y\<bullet>i < b i" |
|
883 |
using * i by (auto simp: box_def) |
|
884 |
moreover have "a i < x\<bullet>i" "x\<bullet>i - a i < e'" |
|
885 |
using a by auto |
|
886 |
moreover have "x\<bullet>i < b i" "b i - x\<bullet>i < e'" |
|
887 |
using b by auto |
|
888 |
ultimately have "\<bar>x\<bullet>i - y\<bullet>i\<bar> < 2 * e'" |
|
889 |
by auto |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
890 |
then have "dist (x \<bullet> i) (y \<bullet> i) < e/sqrt (real (DIM('a)))" |
50087 | 891 |
unfolding e'_def by (auto simp: dist_real_def) |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52625
diff
changeset
|
892 |
then have "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < (e/sqrt (real (DIM('a))))\<^sup>2" |
50087 | 893 |
by (rule power_strict_mono) auto |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52625
diff
changeset
|
894 |
then show "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < e\<^sup>2 / real DIM('a)" |
50087 | 895 |
by (simp add: power_divide) |
896 |
qed auto |
|
53255 | 897 |
also have "\<dots> = e" |
898 |
using `0 < e` by (simp add: real_eq_of_nat) |
|
899 |
finally show "y \<in> ball x e" |
|
900 |
by (auto simp: ball_def) |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
901 |
qed (insert a b, auto simp: box_def) |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
902 |
qed |
51103 | 903 |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
904 |
lemma open_UNION_box: |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
905 |
fixes M :: "'a\<Colon>euclidean_space set" |
53282 | 906 |
assumes "open M" |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
907 |
defines "a' \<equiv> \<lambda>f :: 'a \<Rightarrow> real \<times> real. (\<Sum>(i::'a)\<in>Basis. fst (f i) *\<^sub>R i)" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
908 |
defines "b' \<equiv> \<lambda>f :: 'a \<Rightarrow> real \<times> real. (\<Sum>(i::'a)\<in>Basis. snd (f i) *\<^sub>R i)" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52625
diff
changeset
|
909 |
defines "I \<equiv> {f\<in>Basis \<rightarrow>\<^sub>E \<rat> \<times> \<rat>. box (a' f) (b' f) \<subseteq> M}" |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
910 |
shows "M = (\<Union>f\<in>I. box (a' f) (b' f))" |
52624 | 911 |
proof - |
912 |
{ |
|
913 |
fix x assume "x \<in> M" |
|
914 |
obtain e where e: "e > 0" "ball x e \<subseteq> M" |
|
915 |
using openE[OF `open M` `x \<in> M`] by auto |
|
53282 | 916 |
moreover obtain a b where ab: |
917 |
"x \<in> box a b" |
|
918 |
"\<forall>i \<in> Basis. a \<bullet> i \<in> \<rat>" |
|
919 |
"\<forall>i\<in>Basis. b \<bullet> i \<in> \<rat>" |
|
920 |
"box a b \<subseteq> ball x e" |
|
52624 | 921 |
using rational_boxes[OF e(1)] by metis |
922 |
ultimately have "x \<in> (\<Union>f\<in>I. box (a' f) (b' f))" |
|
923 |
by (intro UN_I[of "\<lambda>i\<in>Basis. (a \<bullet> i, b \<bullet> i)"]) |
|
924 |
(auto simp: euclidean_representation I_def a'_def b'_def) |
|
925 |
} |
|
926 |
then show ?thesis by (auto simp: I_def) |
|
927 |
qed |
|
928 |
||
33175 | 929 |
|
930 |
subsection{* Connectedness *} |
|
931 |
||
932 |
lemma connected_local: |
|
53255 | 933 |
"connected S \<longleftrightarrow> |
934 |
\<not> (\<exists>e1 e2. |
|
935 |
openin (subtopology euclidean S) e1 \<and> |
|
936 |
openin (subtopology euclidean S) e2 \<and> |
|
937 |
S \<subseteq> e1 \<union> e2 \<and> |
|
938 |
e1 \<inter> e2 = {} \<and> |
|
939 |
e1 \<noteq> {} \<and> |
|
940 |
e2 \<noteq> {})" |
|
53282 | 941 |
unfolding connected_def openin_open |
55775 | 942 |
by blast |
33175 | 943 |
|
34105 | 944 |
lemma exists_diff: |
945 |
fixes P :: "'a set \<Rightarrow> bool" |
|
946 |
shows "(\<exists>S. P(- S)) \<longleftrightarrow> (\<exists>S. P S)" (is "?lhs \<longleftrightarrow> ?rhs") |
|
53255 | 947 |
proof - |
948 |
{ |
|
949 |
assume "?lhs" |
|
950 |
then have ?rhs by blast |
|
951 |
} |
|
33175 | 952 |
moreover |
53255 | 953 |
{ |
954 |
fix S |
|
955 |
assume H: "P S" |
|
34105 | 956 |
have "S = - (- S)" by auto |
53255 | 957 |
with H have "P (- (- S))" by metis |
958 |
} |
|
33175 | 959 |
ultimately show ?thesis by metis |
960 |
qed |
|
961 |
||
962 |
lemma connected_clopen: "connected S \<longleftrightarrow> |
|
53255 | 963 |
(\<forall>T. openin (subtopology euclidean S) T \<and> |
964 |
closedin (subtopology euclidean S) T \<longrightarrow> T = {} \<or> T = S)" (is "?lhs \<longleftrightarrow> ?rhs") |
|
965 |
proof - |
|
966 |
have "\<not> connected S \<longleftrightarrow> |
|
967 |
(\<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> {})" |
|
33175 | 968 |
unfolding connected_def openin_open closedin_closed |
55775 | 969 |
by (metis double_complement) |
53282 | 970 |
then have th0: "connected S \<longleftrightarrow> |
53255 | 971 |
\<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> {})" |
52624 | 972 |
(is " _ \<longleftrightarrow> \<not> (\<exists>e2 e1. ?P e2 e1)") |
973 |
apply (simp add: closed_def) |
|
974 |
apply metis |
|
975 |
done |
|
33175 | 976 |
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'))" |
977 |
(is "_ \<longleftrightarrow> \<not> (\<exists>t' t. ?Q t' t)") |
|
978 |
unfolding connected_def openin_open closedin_closed by auto |
|
53255 | 979 |
{ |
980 |
fix e2 |
|
981 |
{ |
|
982 |
fix e1 |
|
53282 | 983 |
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)" |
53255 | 984 |
by auto |
985 |
} |
|
986 |
then have "(\<exists>e1. ?P e2 e1) \<longleftrightarrow> (\<exists>t. ?Q e2 t)" |
|
987 |
by metis |
|
988 |
} |
|
989 |
then have "\<forall>e2. (\<exists>e1. ?P e2 e1) \<longleftrightarrow> (\<exists>t. ?Q e2 t)" |
|
990 |
by blast |
|
991 |
then show ?thesis |
|
992 |
unfolding th0 th1 by simp |
|
33175 | 993 |
qed |
994 |
||
44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
995 |
|
33175 | 996 |
subsection{* Limit points *} |
997 |
||
53282 | 998 |
definition (in topological_space) islimpt:: "'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "islimpt" 60) |
53255 | 999 |
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))" |
33175 | 1000 |
|
1001 |
lemma islimptI: |
|
1002 |
assumes "\<And>T. x \<in> T \<Longrightarrow> open T \<Longrightarrow> \<exists>y\<in>S. y \<in> T \<and> y \<noteq> x" |
|
1003 |
shows "x islimpt S" |
|
1004 |
using assms unfolding islimpt_def by auto |
|
1005 |
||
1006 |
lemma islimptE: |
|
1007 |
assumes "x islimpt S" and "x \<in> T" and "open T" |
|
1008 |
obtains y where "y \<in> S" and "y \<in> T" and "y \<noteq> x" |
|
1009 |
using assms unfolding islimpt_def by auto |
|
1010 |
||
44584 | 1011 |
lemma islimpt_iff_eventually: "x islimpt S \<longleftrightarrow> \<not> eventually (\<lambda>y. y \<notin> S) (at x)" |
1012 |
unfolding islimpt_def eventually_at_topological by auto |
|
1013 |
||
53255 | 1014 |
lemma islimpt_subset: "x islimpt S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> x islimpt T" |
44584 | 1015 |
unfolding islimpt_def by fast |
33175 | 1016 |
|
1017 |
lemma islimpt_approachable: |
|
1018 |
fixes x :: "'a::metric_space" |
|
1019 |
shows "x islimpt S \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e)" |
|
44584 | 1020 |
unfolding islimpt_iff_eventually eventually_at by fast |
33175 | 1021 |
|
1022 |
lemma islimpt_approachable_le: |
|
1023 |
fixes x :: "'a::metric_space" |
|
53640 | 1024 |
shows "x islimpt S \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in> S. x' \<noteq> x \<and> dist x' x \<le> e)" |
33175 | 1025 |
unfolding islimpt_approachable |
44584 | 1026 |
using approachable_lt_le [where f="\<lambda>y. dist y x" and P="\<lambda>y. y \<notin> S \<or> y = x", |
1027 |
THEN arg_cong [where f=Not]] |
|
1028 |
by (simp add: Bex_def conj_commute conj_left_commute) |
|
33175 | 1029 |
|
44571 | 1030 |
lemma islimpt_UNIV_iff: "x islimpt UNIV \<longleftrightarrow> \<not> open {x}" |
1031 |
unfolding islimpt_def by (safe, fast, case_tac "T = {x}", fast, fast) |
|
1032 |
||
51351 | 1033 |
lemma islimpt_punctured: "x islimpt S = x islimpt (S-{x})" |
1034 |
unfolding islimpt_def by blast |
|
1035 |
||
44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
1036 |
text {* A perfect space has no isolated points. *} |
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
1037 |
|
44571 | 1038 |
lemma islimpt_UNIV [simp, intro]: "(x::'a::perfect_space) islimpt UNIV" |
1039 |
unfolding islimpt_UNIV_iff by (rule not_open_singleton) |
|
33175 | 1040 |
|
1041 |
lemma perfect_choose_dist: |
|
44072
5b970711fb39
class perfect_space inherits from topological_space;
huffman
parents:
43338
diff
changeset
|
1042 |
fixes x :: "'a::{perfect_space, metric_space}" |
33175 | 1043 |
shows "0 < r \<Longrightarrow> \<exists>a. a \<noteq> x \<and> dist a x < r" |
53255 | 1044 |
using islimpt_UNIV [of x] |
1045 |
by (simp add: islimpt_approachable) |
|
33175 | 1046 |
|
1047 |
lemma closed_limpt: "closed S \<longleftrightarrow> (\<forall>x. x islimpt S \<longrightarrow> x \<in> S)" |
|
1048 |
unfolding closed_def |
|
1049 |
apply (subst open_subopen) |
|
34105 | 1050 |
apply (simp add: islimpt_def subset_eq) |
52624 | 1051 |
apply (metis ComplE ComplI) |
1052 |
done |
|
33175 | 1053 |
|
1054 |
lemma islimpt_EMPTY[simp]: "\<not> x islimpt {}" |
|
1055 |
unfolding islimpt_def by auto |
|
1056 |
||
1057 |
lemma finite_set_avoid: |
|
1058 |
fixes a :: "'a::metric_space" |
|
53255 | 1059 |
assumes fS: "finite S" |
53640 | 1060 |
shows "\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<longrightarrow> d \<le> dist a x" |
53255 | 1061 |
proof (induct rule: finite_induct[OF fS]) |
1062 |
case 1 |
|
1063 |
then show ?case by (auto intro: zero_less_one) |
|
33175 | 1064 |
next |
1065 |
case (2 x F) |
|
53255 | 1066 |
from 2 obtain d where d: "d >0" "\<forall>x\<in>F. x\<noteq>a \<longrightarrow> d \<le> dist a x" |
1067 |
by blast |
|
1068 |
show ?case |
|
1069 |
proof (cases "x = a") |
|
1070 |
case True |
|
1071 |
then show ?thesis using d by auto |
|
1072 |
next |
|
1073 |
case False |
|
33175 | 1074 |
let ?d = "min d (dist a x)" |
53255 | 1075 |
have dp: "?d > 0" |
1076 |
using False d(1) using dist_nz by auto |
|
1077 |
from d have d': "\<forall>x\<in>F. x\<noteq>a \<longrightarrow> ?d \<le> dist a x" |
|
1078 |
by auto |
|
1079 |
with dp False show ?thesis |
|
1080 |
by (auto intro!: exI[where x="?d"]) |
|
1081 |
qed |
|
33175 | 1082 |
qed |
1083 |
||
1084 |
lemma islimpt_Un: "x islimpt (S \<union> T) \<longleftrightarrow> x islimpt S \<or> x islimpt T" |
|
50897
078590669527
generalize lemma islimpt_finite to class t1_space
huffman
parents:
50884
diff
changeset
|
1085 |
by (simp add: islimpt_iff_eventually eventually_conj_iff) |
33175 | 1086 |
|
1087 |
lemma discrete_imp_closed: |
|
1088 |
fixes S :: "'a::metric_space set" |
|
53255 | 1089 |
assumes e: "0 < e" |
1090 |
and d: "\<forall>x \<in> S. \<forall>y \<in> S. dist y x < e \<longrightarrow> y = x" |
|
33175 | 1091 |
shows "closed S" |
53255 | 1092 |
proof - |
1093 |
{ |
|
1094 |
fix x |
|
1095 |
assume C: "\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e" |
|
33175 | 1096 |
from e have e2: "e/2 > 0" by arith |
53282 | 1097 |
from C[rule_format, OF e2] obtain y where y: "y \<in> S" "y \<noteq> x" "dist y x < e/2" |
53255 | 1098 |
by blast |
33175 | 1099 |
let ?m = "min (e/2) (dist x y) " |
53255 | 1100 |
from e2 y(2) have mp: "?m > 0" |
53291 | 1101 |
by (simp add: dist_nz[symmetric]) |
53282 | 1102 |
from C[rule_format, OF mp] obtain z where z: "z \<in> S" "z \<noteq> x" "dist z x < ?m" |
53255 | 1103 |
by blast |
33175 | 1104 |
have th: "dist z y < e" using z y |
1105 |
by (intro dist_triangle_lt [where z=x], simp) |
|
1106 |
from d[rule_format, OF y(1) z(1) th] y z |
|
1107 |
have False by (auto simp add: dist_commute)} |
|
53255 | 1108 |
then show ?thesis |
1109 |
by (metis islimpt_approachable closed_limpt [where 'a='a]) |
|
33175 | 1110 |
qed |
1111 |
||
44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
1112 |
|
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
1113 |
subsection {* Interior of a Set *} |
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset
|
1114 |
|
44519 | 1115 |
definition "interior S = \<Union>{T. open T \<and> T \<subseteq> S}" |
1116 |
||
1117 |
lemma interiorI [intro?]: |
|
1118 |
assumes "open T" and "x \<in> T" and "T \<subseteq> S" |
|
1119 |
shows "x \<in> interior S" |
|
1120 |
using assms unfolding interior_def by fast |
|
1121 |
||
1122 |
lemma interiorE [elim?]: |
|
1123 |
assumes "x \<in> interior S" |
|
1124 |
obtains T where "open T" and "x \<in> T" and "T \<subseteq> S" |
|
1125 |
using assms unfolding interior_def by fast |
|
1126 |
||
1127 |
lemma open_interior [simp, intro]: "open (interior S)" |
|
1128 |
by (simp add: interior_def open_Union) |
|
1129 |
||
1130 |
lemma interior_subset: "interior S \<subseteq> S" |
|
1131 |
by (auto simp add: interior_def) |
|
1132 |
||
1133 |
lemma interior_maximal: "T \<subseteq> S \<Longrightarrow> open T \<Longrightarrow> T \<subseteq> interior S" |
|
1134 |
by (auto simp add: interior_def) |
|
1135 |
||
1136 |
lemma interior_open: "open S \<Longrightarrow> interior S = S" |
|
1137 |
by (intro equalityI interior_subset interior_maximal subset_refl) |
|
33175 | 1138 |
|
1139 |
lemma interior_eq: "interior S = S \<longleftrightarrow> open S" |
|
44519 | 1140 |
by (metis open_interior interior_open) |
1141 |
||
1142 |