author  wenzelm 
Thu, 29 Aug 2013 00:18:02 +0200  
changeset 53255  addd7b9b2bff 
parent 53015  a1119cf551e8 
child 53282  9d6e263fa921 
permissions  rwrr 
33714
eb2574ac4173
Added new lemmas to Euclidean Space by Robert Himmelmann
hoelzl
parents:
33324
diff
changeset

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

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

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

8 

9 
theory Topology_Euclidean_Space 

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

12 
"~~/src/HOL/Library/Countable_Set" 
50087  13 
"~~/src/HOL/Library/Glbs" 
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

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

18 

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

21 
shows "dist 0 x = norm x" 

22 
unfolding dist_norm by simp 

23 

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

24 
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

25 
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

26 

50972  27 
(* LEGACY *) 
28 
lemma lim_subseq: "subseq r \<Longrightarrow> s > l \<Longrightarrow> (s o r) > l" 

29 
by (rule LIMSEQ_subseq_LIMSEQ) 

30 

51342  31 
lemmas real_isGlb_unique = isGlb_unique[where 'a=real] 
50942  32 

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

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

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

35 
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

36 

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

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

38 
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

39 
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

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

41 

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

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

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

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

45 

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

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

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

48 
\<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

49 
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

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

51 

53255  52 

50087  53 
subsection {* Topological Basis *} 
54 

55 
context topological_space 

56 
begin 

57 

58 
definition "topological_basis B = 

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

59 
((\<forall>b\<in>B. open b) \<and> (\<forall>x. open x \<longrightarrow> (\<exists>B'. B' \<subseteq> B \<and> \<Union>B' = x)))" 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

60 

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

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

62 
"topological_basis B = (\<forall>x. open x \<longleftrightarrow> (\<exists>B'. B' \<subseteq> B \<and> \<Union>B' = x))" 
50998  63 
unfolding topological_basis_def 
64 
apply safe 

65 
apply fastforce 

66 
apply fastforce 

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

68 
apply simp 

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

70 
apply auto 

71 
done 

72 

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

75 
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'))" 

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

77 
proof safe 

78 
fix O' and x::'a 

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

80 
hence "(\<exists>B'\<subseteq>B. \<Union>B' = O')" by (simp add: topological_basis_def) 

81 
then obtain B' where "B' \<subseteq> B" "O' = \<Union>B'" by auto 

82 
thus "\<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'" using H by auto 

83 
next 

84 
assume H: ?rhs 

85 
show "topological_basis B" using assms unfolding topological_basis_def 

86 
proof safe 

87 
fix O'::"'a set" assume "open O'" 

88 
with H obtain f where "\<forall>x\<in>O'. f x \<in> B \<and> x \<in> f x \<and> f x \<subseteq> O'" 

89 
by (force intro: bchoice simp: Bex_def) 

90 
thus "\<exists>B'\<subseteq>B. \<Union>B' = O'" 

91 
by (auto intro: exI[where x="{f x x. x \<in> O'}"]) 

92 
qed 

93 
qed 

94 

95 
lemma topological_basisI: 

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

97 
assumes "\<And>O' x. open O' \<Longrightarrow> x \<in> O' \<Longrightarrow> \<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'" 

98 
shows "topological_basis B" 

99 
using assms by (subst topological_basis_iff) auto 

100 

101 
lemma topological_basisE: 

102 
fixes O' 

103 
assumes "topological_basis B" 

104 
assumes "open O'" 

105 
assumes "x \<in> O'" 

106 
obtains B' where "B' \<in> B" "x \<in> B'" "B' \<subseteq> O'" 

107 
proof atomize_elim 

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

109 
with topological_basis_iff assms 

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

111 
qed 

112 

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

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

114 
assumes "topological_basis B" 
84ddcf5364b4
allow arbitrary enumerations of basis in locale for generation of borel sets
immler
parents:
50087
diff
changeset

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

116 
shows "open X" 
84ddcf5364b4
allow arbitrary enumerations of basis in locale for generation of borel sets
immler
parents:
50087
diff
changeset

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

118 
by (simp add: topological_basis_def) 
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: 
53255  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'" 
50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

142 
shows "(\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>B' \<in> B. f B' \<in> X))" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

143 
proof (intro allI impI) 
53255  144 
fix X::"'a set" 
145 
assume "open X" "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> {}`]] 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

147 
guess B' . note B' = this 
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) 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

169 
moreover from topological_basisE[OF A a] guess A0 . 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

170 
moreover from topological_basisE[OF B b] guess B0 . 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

171 
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

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

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

174 
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

175 

53255  176 

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

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

178 

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

179 
locale countable_basis = 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

180 
fixes B::"'a::topological_space set set" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

181 
assumes is_basis: "topological_basis B" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

182 
assumes countable_basis: "countable B" 
33175  183 
begin 
184 

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

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

187 
shows "\<exists>B' \<subseteq> B. X = Union B'" 
53255  188 
using assms countable_basis is_basis 
189 
unfolding topological_basis_def by blast 

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

190 

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

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

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

193 
obtains B' where "B' \<subseteq> B" "X = Union B'" 
53255  194 
using assms open_countable_basis_ex 
195 
by (atomize_elim) simp 

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

196 

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

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

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

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

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

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

203 
by (intro exI[where x="?f ` B"]) (metis (mono_tags) all_not_in_conv imageI someI) 
50087  204 
qed 
205 

206 
lemma countable_dense_setE: 

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

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

208 
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

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

210 

50087  211 
end 
212 

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

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

216 
using first_countable_basis[of x] 

51473  217 
apply atomize_elim 
218 
apply (elim exE) 

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

220 
apply auto 

221 
done 

50883  222 

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

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

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

227 
proof atomize_elim 

228 
from first_countable_basisE[of x] guess A' . note A' = this 

229 
def A \<equiv> "(\<lambda>N. \<Inter>((\<lambda>n. from_nat_into A' n) ` N)) ` (Collect finite::nat set set)" 

53255  230 
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  231 
(\<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)" 
232 
proof (safe intro!: exI[where x=A]) 

53255  233 
show "countable A" 
234 
unfolding A_def by (intro countable_image countable_Collect_finite) 

235 
fix a 

236 
assume "a \<in> A" 

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

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

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

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

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

244 
by (auto simp: A_def) 

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

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

51105  247 
next 
53255  248 
fix S 
249 
assume "open S" "x \<in> S" 

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

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

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

254 
qed 

255 

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

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

51473  260 
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))" 
261 
proof (safe intro!: exI[of _ "from_nat_into A"]) 

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

266 
next 

267 
fix S 

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

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

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

51473  271 
qed 
51350  272 

50883  273 
instance prod :: (first_countable_topology, first_countable_topology) first_countable_topology 
274 
proof 

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

276 
from first_countable_basisE[of "fst x"] guess A :: "'a set set" . note A = this 

277 
from first_countable_basisE[of "snd x"] guess B :: "'b set set" . note B = this 

51473  278 
show "\<exists>A::nat \<Rightarrow> ('a \<times> 'b) 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))" 
279 
proof (rule first_countableI[of "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"], safe) 

53255  280 
fix a b 
281 
assume x: "a \<in> A" "b \<in> B" 

50883  282 
with A(2, 3)[of a] B(2, 3)[of b] show "x \<in> a \<times> b" "open (a \<times> b)" 
283 
unfolding mem_Times_iff by (auto intro: open_Times) 

284 
next 

53255  285 
fix S 
286 
assume "open S" "x \<in> S" 

50883  287 
from open_prod_elim[OF this] guess a' b' . 
288 
moreover with A(4)[of a'] B(4)[of b'] 

289 
obtain a b where "a \<in> A" "a \<subseteq> a'" "b \<in> B" "b \<subseteq> b'" by auto 

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

291 
by (auto intro!: bexI[of _ "a \<times> b"] bexI[of _ a] bexI[of _ b]) 

292 
qed (simp add: A B) 

293 
qed 

294 

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

295 
class second_countable_topology = topological_space + 
51343
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

296 
assumes ex_countable_subbasis: "\<exists>B::'a::topological_space 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

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

298 

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

299 
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

300 
proof  
53255  301 
from ex_countable_subbasis obtain B where B: "countable B" "open = generate_topology B" 
302 
by blast 

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

303 
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

304 

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

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

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

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

308 
by (intro countable_image countable_Collect_finite_subset B) 
53255  309 
{ 
310 
fix S 

311 
assume "open S" 

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

312 
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

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

314 
proof induct 
53255  315 
case UNIV 
316 
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

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

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

319 
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

320 
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

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

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

323 
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

324 
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

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

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

327 
then have "\<forall>k\<in>K. \<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. UNION B' Inter = k" by auto 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

328 
then guess k unfolding bchoice_iff .. 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

329 
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

330 
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

331 
next 
53255  332 
case (Basis S) 
333 
then show ?case 

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

334 
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

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

336 
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

337 
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

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

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

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

341 
(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

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

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

344 

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

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

346 

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

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

348 
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

349 
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

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

351 

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

352 
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

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

354 
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

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

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

357 
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

358 
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

359 
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

360 
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

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

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

363 

50883  364 
instance second_countable_topology \<subseteq> first_countable_topology 
365 
proof 

366 
fix x :: 'a 

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

368 
then have B: "countable B" "topological_basis B" 

369 
using countable_basis is_basis 

370 
by (auto simp: countable_basis is_basis) 

51473  371 
then show "\<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))" 
372 
by (intro first_countableI[of "{b\<in>B. x \<in> b}"]) 

373 
(fastforce simp: topological_space_class.topological_basis_def)+ 

50883  374 
qed 
375 

53255  376 

50087  377 
subsection {* Polish spaces *} 
378 

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

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

381 

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

382 
class polish_space = complete_space + second_countable_topology 
50087  383 

44517  384 
subsection {* General notion of a topology as a value *} 
33175  385 

53255  386 
definition "istopology L \<longleftrightarrow> 
387 
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))" 

388 

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

392 

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

394 
using openin[of U] by blast 

395 

396 
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

397 
using topology_inverse[unfolded mem_Collect_eq] . 
33175  398 

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

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

401 

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

53255  403 
proof 
404 
assume "T1 = T2" 

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

406 
next 

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

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

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

410 
then show "T1 = T2" unfolding openin_inverse . 

33175  411 
qed 
412 

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

414 

415 
definition "topspace T = \<Union>{S. openin T S}" 

416 

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

417 
subsubsection {* Main properties of open sets *} 
33175  418 

419 
lemma openin_clauses: 

420 
fixes U :: "'a topology" 

421 
shows "openin U {}" 

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

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

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

424 
using openin[of U] unfolding istopology_def mem_Collect_eq 
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

425 
by fast+ 
33175  426 

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

428 
unfolding topspace_def by blast 

53255  429 

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

431 
by (simp add: openin_clauses) 

33175  432 

433 
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

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

435 

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

436 
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

437 
using openin_clauses by simp 
33175  438 

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

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

441 

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

33175  444 

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

36584  447 
proof 
49711  448 
assume ?lhs 
449 
then show ?rhs by auto 

36584  450 
next 
451 
assume H: ?rhs 

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

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

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

455 
finally show "openin U S" . 

33175  456 
qed 
457 

49711  458 

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

459 
subsubsection {* Closed sets *} 
33175  460 

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

462 

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

465 

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

467 
by (simp add: closedin_def) 

468 

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

470 
by (simp add: closedin_def) 

471 

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

474 

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

477 

478 
lemma closedin_Inter[intro]: 

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

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

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

482 
using Ke Kc unfolding closedin_def Diff_Inter by auto 

33175  483 

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

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

486 

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

489 

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

492 
apply (metis openin_subset subset_eq) 

493 
done 

494 

53255  495 
lemma openin_closedin: "S \<subseteq> topspace U \<Longrightarrow> (openin U S \<longleftrightarrow> closedin U (topspace U  S))" 
33175  496 
by (simp add: openin_closedin_eq) 
497 

53255  498 
lemma openin_diff[intro]: 
499 
assumes oS: "openin U S" 

500 
and cT: "closedin U T" 

501 
shows "openin U (S  T)" 

502 
proof  

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

505 
then show ?thesis using oS cT by (auto simp add: closedin_def) 

506 
qed 

507 

53255  508 
lemma closedin_diff[intro]: 
509 
assumes oS: "closedin U S" 

510 
and cT: "openin U T" 

511 
shows "closedin U (S  T)" 

512 
proof  

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

514 
using closedin_subset[of U S] oS cT 

515 
by (auto simp add: topspace_def) 

516 
then show ?thesis 

517 
using oS cT by (auto simp add: openin_closedin_eq) 

518 
qed 

519 

33175  520 

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

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

522 

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

523 
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

524 

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

525 
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

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

528 
have "?L {}" by blast 
53255  529 
{ 
530 
fix A B 

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

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

533 
by blast 

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

535 
using Sa Sb by blast+ 

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

537 
} 

33175  538 
moreover 
53255  539 
{ 
540 
fix K assume K: "K \<subseteq> Collect ?L" 

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

541 
have th0: "Collect ?L = (\<lambda>S. S \<inter> V) ` Collect (openin U)" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

542 
apply (rule set_eqI) 
33175  543 
apply (simp add: Ball_def image_iff) 
53255  544 
apply metis 
545 
done 

33175  546 
from K[unfolded th0 subset_image_iff] 
53255  547 
obtain Sk where Sk: "Sk \<subseteq> Collect (openin U)" "K = (\<lambda>S. S \<inter> V) ` Sk" 
548 
by blast 

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

550 
using Sk by auto 

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

552 
using Sk by (auto simp add: subset_eq) 

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

554 
} 

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

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

556 
unfolding subset_eq mem_Collect_eq istopology_def by blast 
33175  557 
qed 
558 

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

561 
by auto 
33175  562 

53255  563 
lemma topspace_subtopology: "topspace (subtopology U V) = topspace U \<inter> V" 
33175  564 
by (auto simp add: topspace_def openin_subtopology) 
565 

53255  566 
lemma closedin_subtopology: "closedin (subtopology U V) S \<longleftrightarrow> (\<exists>T. closedin U T \<and> S = T \<inter> V)" 
33175  567 
unfolding closedin_def topspace_subtopology 
568 
apply (simp add: openin_subtopology) 

569 
apply (rule iffI) 

570 
apply clarify 

571 
apply (rule_tac x="topspace U  T" in exI) 

53255  572 
apply auto 
573 
done 

33175  574 

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

576 
unfolding openin_subtopology 

577 
apply (rule iffI, clarify) 

53255  578 
apply (frule openin_subset[of U]) 
579 
apply blast 

33175  580 
apply (rule exI[where x="topspace U"]) 
49711  581 
apply auto 
582 
done 

583 

584 
lemma subtopology_superset: 

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

33175  586 
shows "subtopology U V = U" 
53255  587 
proof  
588 
{ 

589 
fix S 

590 
{ 

591 
fix T 

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

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

594 
by blast 

595 
have "openin U S" 

596 
unfolding eq using T by blast 

597 
} 

33175  598 
moreover 
53255  599 
{ 
600 
assume S: "openin U S" 

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

602 
using openin_subset[OF S] UV by auto 

603 
} 

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

605 
by blast 

606 
} 

607 
then show ?thesis 

608 
unfolding topology_eq openin_subtopology by blast 

33175  609 
qed 
610 

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

612 
by (simp add: subtopology_superset) 

613 

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

615 
by (simp add: subtopology_superset) 

616 

53255  617 

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

618 
subsubsection {* The standard Euclidean topology *} 
33175  619 

53255  620 
definition euclidean :: "'a::topological_space topology" 
621 
where "euclidean = topology open" 

33175  622 

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

624 
unfolding euclidean_def 

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

626 
apply (rule topology_inverse[symmetric]) 

627 
apply (auto simp add: istopology_def) 

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

628 
done 
33175  629 

630 
lemma topspace_euclidean: "topspace euclidean = UNIV" 

631 
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

632 
apply (rule set_eqI) 
53255  633 
apply (auto simp add: open_openin[symmetric]) 
634 
done 

33175  635 

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

637 
by (simp add: topspace_euclidean topspace_subtopology) 

638 

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

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

641 

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

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

644 

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

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

646 

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

647 
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

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

649 

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

650 
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

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

652 

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

653 
lemma open_openin_trans[trans]: 
53255  654 
"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

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

656 

53255  657 
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

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

659 

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

660 
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

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

662 

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

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

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

665 

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

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

667 
apply (subgoal_tac "S \<inter> T = T" ) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

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

669 
apply (frule closedin_closed_Int[of T S]) 
52624  670 
apply simp 
671 
done 

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

672 

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

673 
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

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

675 

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

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

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

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

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

681 
proof 
53255  682 
assume ?lhs 
683 
then show ?rhs unfolding openin_open open_dist by blast 

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

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

685 
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

686 
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

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

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

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

690 
apply (clarsimp simp add: less_diff_eq) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

691 
apply (erule rev_bexI) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

692 
apply (rule_tac x=d in exI, clarify) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

693 
apply (erule le_less_trans [OF dist_triangle]) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

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

695 
assume ?rhs hence 2: "S = U \<inter> T" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

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

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

698 
apply (drule (1) bspec, erule rev_bexI) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

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

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

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

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

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

704 

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

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

706 

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

709 
openin (subtopology euclidean U) S" 

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

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

711 

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

712 
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

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

714 

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

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

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

718 
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

719 

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

720 
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

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

722 

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 
subsection {* Open and closed balls *} 
33175  725 

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

728 

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

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

33175  731 

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

732 
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

733 
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

734 

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

735 
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

736 
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

737 

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

738 
lemma mem_ball_0: 
33175  739 
fixes x :: "'a::real_normed_vector" 
740 
shows "x \<in> ball 0 e \<longleftrightarrow> norm x < e" 

741 
by (simp add: dist_norm) 

742 

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

743 
lemma mem_cball_0: 
33175  744 
fixes x :: "'a::real_normed_vector" 
745 
shows "x \<in> cball 0 e \<longleftrightarrow> norm x \<le> e" 

746 
by (simp add: dist_norm) 

747 

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

748 
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

749 
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

750 

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

751 
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

752 
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

753 

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

756 

757 
lemma subset_ball[intro]: "d <= e ==> ball x d \<subseteq> ball x e" 

758 
by (simp add: subset_eq) 

759 

760 
lemma subset_cball[intro]: "d <= e ==> cball x d \<subseteq> cball x e" 

761 
by (simp add: subset_eq) 

762 

33175  763 
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

764 
by (simp add: set_eq_iff) arith 
33175  765 

766 
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

767 
by (simp add: set_eq_iff) 
33175  768 

53255  769 
lemma diff_less_iff: 
770 
"(a::real)  b > 0 \<longleftrightarrow> a > b" 

33175  771 
"(a::real)  b < 0 \<longleftrightarrow> a < b" 
53255  772 
"a  b < c \<longleftrightarrow> a < c + b" "a  b > c \<longleftrightarrow> a > c + b" 
773 
by arith+ 

774 

775 
lemma diff_le_iff: 

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

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

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

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

780 
by arith+ 

33175  781 

782 
lemma open_ball[intro, simp]: "open (ball x e)" 

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

783 
unfolding open_dist ball_def mem_Collect_eq Ball_def 
33175  784 
unfolding dist_commute 
785 
apply clarify 

786 
apply (rule_tac x="e  dist xa x" in exI) 

787 
using dist_triangle_alt[where z=x] 

788 
apply (clarsimp simp add: diff_less_iff) 

789 
apply atomize 

790 
apply (erule_tac x="y" in allE) 

791 
apply (erule_tac x="xa" in allE) 

52624  792 
apply arith 
793 
done 

33175  794 

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

796 
unfolding open_dist subset_eq mem_ball Ball_def dist_commute .. 

797 

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

798 
lemma openE[elim?]: 
eb2574ac4173
Added new lemmas to Euclidean Space by Robert Himmelmann
hoelzl
parents:
33324
diff
changeset

799 
assumes "open S" "x\<in>S" 
eb2574ac4173
Added new lemmas to Euclidean Space by Robert Himmelmann
hoelzl
parents:
33324
diff
changeset

800 
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

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

802 

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

805 

806 
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

807 
unfolding mem_ball set_eq_iff 
33175  808 
apply (simp add: not_less) 
52624  809 
apply (metis zero_le_dist order_trans dist_self) 
810 
done 

33175  811 

812 
lemma ball_empty[intro]: "e \<le> 0 ==> ball x e = {}" by simp 

813 

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

814 
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

815 
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

816 
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

817 
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

818 
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

819 

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 
definition "box a b = {x. \<forall>i\<in>Basis. a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> 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

821 

50087  822 
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

823 
fixes x :: "'a\<Colon>euclidean_space" 
50087  824 
assumes "0 < 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

825 
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  826 
proof  
827 
def e' \<equiv> "e / (2 * sqrt (real (DIM ('a))))" 

53255  828 
then have e: "0 < e'" 
829 
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

830 
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  831 
proof 
53255  832 
fix i 
833 
from Rats_dense_in_real[of "x \<bullet> i  e'" "x \<bullet> i"] e 

834 
show "?th i" by auto 

50087  835 
qed 
836 
from choice[OF this] guess a .. note a = this 

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

837 
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  838 
proof 
53255  839 
fix i 
840 
from Rats_dense_in_real[of "x \<bullet> i" "x \<bullet> i + e'"] e 

841 
show "?th i" by auto 

50087  842 
qed 
843 
from choice[OF this] guess b .. note b = this 

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

844 
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

845 
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

846 
proof (rule exI[of _ ?a], rule exI[of _ ?b], safe) 
53255  847 
fix y :: 'a 
848 
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

849 
have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)" 
50087  850 
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

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

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

856 
using * i by (auto simp: box_def) 

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

858 
using a by auto 

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

860 
using b by auto 

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

862 
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

863 
then have "dist (x \<bullet> i) (y \<bullet> i) < e/sqrt (real (DIM('a)))" 
50087  864 
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

865 
then have "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < (e/sqrt (real (DIM('a))))\<^sup>2" 
50087  866 
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

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

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

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

873 
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

874 
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

875 
qed 
51103  876 

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

877 
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

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

879 
assumes "open M" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

880 
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

881 
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

882 
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

883 
shows "M = (\<Union>f\<in>I. box (a' f) (b' f))" 
52624  884 
proof  
885 
{ 

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

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

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

889 
moreover then obtain a b where ab: "x \<in> box a b" 

890 
"\<forall>i \<in> Basis. a \<bullet> i \<in> \<rat>" "\<forall>i\<in>Basis. b \<bullet> i \<in> \<rat>" "box a b \<subseteq> ball x e" 

891 
using rational_boxes[OF e(1)] by metis 

892 
ultimately have "x \<in> (\<Union>f\<in>I. box (a' f) (b' f))" 

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

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

895 
} 

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

897 
qed 

898 

33175  899 

900 
subsection{* Connectedness *} 

901 

902 
lemma connected_local: 

53255  903 
"connected S \<longleftrightarrow> 
904 
\<not> (\<exists>e1 e2. 

905 
openin (subtopology euclidean S) e1 \<and> 

906 
openin (subtopology euclidean S) e2 \<and> 

907 
S \<subseteq> e1 \<union> e2 \<and> 

908 
e1 \<inter> e2 = {} \<and> 

909 
e1 \<noteq> {} \<and> 

910 
e2 \<noteq> {})" 

911 
unfolding connected_def openin_open by (safe, blast+) 

33175  912 

34105  913 
lemma exists_diff: 
914 
fixes P :: "'a set \<Rightarrow> bool" 

915 
shows "(\<exists>S. P( S)) \<longleftrightarrow> (\<exists>S. P S)" (is "?lhs \<longleftrightarrow> ?rhs") 

53255  916 
proof  
917 
{ 

918 
assume "?lhs" 

919 
then have ?rhs by blast 

920 
} 

33175  921 
moreover 
53255  922 
{ 
923 
fix S 

924 
assume H: "P S" 

34105  925 
have "S =  ( S)" by auto 
53255  926 
with H have "P ( ( S))" by metis 
927 
} 

33175  928 
ultimately show ?thesis by metis 
929 
qed 

930 

931 
lemma connected_clopen: "connected S \<longleftrightarrow> 

53255  932 
(\<forall>T. openin (subtopology euclidean S) T \<and> 
933 
closedin (subtopology euclidean S) T \<longrightarrow> T = {} \<or> T = S)" (is "?lhs \<longleftrightarrow> ?rhs") 

934 
proof  

935 
have "\<not> connected S \<longleftrightarrow> 

936 
(\<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  937 
unfolding connected_def openin_open closedin_closed 
52624  938 
apply (subst exists_diff) 
939 
apply blast 

940 
done 

53255  941 
hence th0: "connected S \<longleftrightarrow> 
942 
\<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  943 
(is " _ \<longleftrightarrow> \<not> (\<exists>e2 e1. ?P e2 e1)") 
944 
apply (simp add: closed_def) 

945 
apply metis 

946 
done 

33175  947 
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'))" 
948 
(is "_ \<longleftrightarrow> \<not> (\<exists>t' t. ?Q t' t)") 

949 
unfolding connected_def openin_open closedin_closed by auto 

53255  950 
{ 
951 
fix e2 

952 
{ 

953 
fix e1 

954 
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)" 

955 
by auto 

956 
} 

957 
then have "(\<exists>e1. ?P e2 e1) \<longleftrightarrow> (\<exists>t. ?Q e2 t)" 

958 
by metis 

959 
} 

960 
then have "\<forall>e2. (\<exists>e1. ?P e2 e1) \<longleftrightarrow> (\<exists>t. ?Q e2 t)" 

961 
by blast 

962 
then show ?thesis 

963 
unfolding th0 th1 by simp 

33175  964 
qed 
965 

52624  966 
lemma connected_empty[simp, intro]: "connected {}" (* FIXME duplicate? *) 
967 
by simp 

33175  968 

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

969 

33175  970 
subsection{* Limit points *} 
971 

53255  972 
definition (in topological_space) islimpt:: "'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "islimpt" 60) 
973 
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  974 

975 
lemma islimptI: 

976 
assumes "\<And>T. x \<in> T \<Longrightarrow> open T \<Longrightarrow> \<exists>y\<in>S. y \<in> T \<and> y \<noteq> x" 

977 
shows "x islimpt S" 

978 
using assms unfolding islimpt_def by auto 

979 

980 
lemma islimptE: 

981 
assumes "x islimpt S" and "x \<in> T" and "open T" 

982 
obtains y where "y \<in> S" and "y \<in> T" and "y \<noteq> x" 

983 
using assms unfolding islimpt_def by auto 

984 

44584  985 
lemma islimpt_iff_eventually: "x islimpt S \<longleftrightarrow> \<not> eventually (\<lambda>y. y \<notin> S) (at x)" 
986 
unfolding islimpt_def eventually_at_topological by auto 

987 

53255  988 
lemma islimpt_subset: "x islimpt S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> x islimpt T" 
44584  989 
unfolding islimpt_def by fast 
33175  990 

991 
lemma islimpt_approachable: 

992 
fixes x :: "'a::metric_space" 

993 
shows "x islimpt S \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e)" 

44584  994 
unfolding islimpt_iff_eventually eventually_at by fast 
33175  995 

996 
lemma islimpt_approachable_le: 

997 
fixes x :: "'a::metric_space" 

998 
shows "x islimpt S \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in> S. x' \<noteq> x \<and> dist x' x <= e)" 

999 
unfolding islimpt_approachable 

44584  1000 
using approachable_lt_le [where f="\<lambda>y. dist y x" and P="\<lambda>y. y \<notin> S \<or> y = x", 
1001 
THEN arg_cong [where f=Not]] 

1002 
by (simp add: Bex_def conj_commute conj_left_commute) 

33175  1003 

44571  1004 
lemma islimpt_UNIV_iff: "x islimpt UNIV \<longleftrightarrow> \<not> open {x}" 
1005 
unfolding islimpt_def by (safe, fast, case_tac "T = {x}", fast, fast) 

1006 

51351  1007 
lemma islimpt_punctured: "x islimpt S = x islimpt (S{x})" 
1008 
unfolding islimpt_def by blast 

1009 

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

1010 
text {* A perfect space has no isolated points. *} 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

1011 

44571  1012 
lemma islimpt_UNIV [simp, intro]: "(x::'a::perfect_space) islimpt UNIV" 
1013 
unfolding islimpt_UNIV_iff by (rule not_open_singleton) 

33175  1014 

1015 
lemma perfect_choose_dist: 

44072
5b970711fb39
class perfect_space inherits from topological_space;
huffman
parents:
43338
diff
changeset

1016 
fixes x :: "'a::{perfect_space, metric_space}" 
33175  1017 
shows "0 < r \<Longrightarrow> \<exists>a. a \<noteq> x \<and> dist a x < r" 
53255  1018 
using islimpt_UNIV [of x] 
1019 
by (simp add: islimpt_approachable) 

33175  1020 

1021 
lemma closed_limpt: "closed S \<longleftrightarrow> (\<forall>x. x islimpt S \<longrightarrow> x \<in> S)" 

1022 
unfolding closed_def 

1023 
apply (subst open_subopen) 

34105  1024 
apply (simp add: islimpt_def subset_eq) 
52624  1025 
apply (metis ComplE ComplI) 
1026 
done 

33175  1027 

1028 
lemma islimpt_EMPTY[simp]: "\<not> x islimpt {}" 

1029 
unfolding islimpt_def by auto 

1030 

1031 
lemma finite_set_avoid: 

1032 
fixes a :: "'a::metric_space" 

53255  1033 
assumes fS: "finite S" 
1034 
shows "\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<longrightarrow> d <= dist a x" 

1035 
proof (induct rule: finite_induct[OF fS]) 

1036 
case 1 

1037 
then show ?case by (auto intro: zero_less_one) 

33175  1038 
next 
1039 
case (2 x F) 

53255  1040 
from 2 obtain d where d: "d >0" "\<forall>x\<in>F. x\<noteq>a \<longrightarrow> d \<le> dist a x" 
1041 
by blast 

1042 
show ?case 

1043 
proof (cases "x = a") 

1044 
case True 

1045 
then show ?thesis using d by auto 

1046 
next 

1047 
case False 

33175  1048 
let ?d = "min d (dist a x)" 
53255  1049 
have dp: "?d > 0" 
1050 
using False d(1) using dist_nz by auto 

1051 
from d have d': "\<forall>x\<in>F. x\<noteq>a \<longrightarrow> ?d \<le> dist a x" 

1052 
by auto 

1053 
with dp False show ?thesis 

1054 
by (auto intro!: exI[where x="?d"]) 

1055 
qed 

33175  1056 
qed 
1057 

1058 
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

1059 
by (simp add: islimpt_iff_eventually eventually_conj_iff) 
33175  1060 

1061 
lemma discrete_imp_closed: 

1062 
fixes S :: "'a::metric_space set" 

53255  1063 
assumes e: "0 < e" 
1064 
and d: "\<forall>x \<in> S. \<forall>y \<in> S. dist y x < e \<longrightarrow> y = x" 

33175  1065 
shows "closed S" 
53255  1066 
proof  
1067 
{ 

1068 
fix x 

1069 
assume C: "\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e" 

33175  1070 
from e have e2: "e/2 > 0" by arith 
53255  1071 
from C[rule_format, OF e2] obtain y where y: "y \<in> S" "y\<noteq>x" "dist y x < e/2" 
1072 
by blast 

33175  1073 
let ?m = "min (e/2) (dist x y) " 
53255  1074 
from e2 y(2) have mp: "?m > 0" 
1075 
by (simp add: dist_nz[THEN sym]) 

1076 
from C[rule_format, OF mp] obtain z where z: "z \<in> S" "z\<noteq>x" "dist z x < ?m" 

1077 
by blast 

33175  1078 
have th: "dist z y < e" using z y 
1079 
by (intro dist_triangle_lt [where z=x], simp) 

1080 
from d[rule_format, OF y(1) z(1) th] y z 

1081 
have False by (auto simp add: dist_commute)} 

53255  1082 
then show ?thesis 
1083 
by (metis islimpt_approachable closed_limpt [where 'a='a]) 

33175  1084 
qed 
1085 

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

1086 

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

1087 
subsection {* Interior of a Set *} 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

1088 

44519  1089 
definition "interior S = \<Union>{T. open T \<and> T \<subseteq> S}" 
1090 

1091 
lemma interiorI [intro?]: 

1092 
assumes "open T" and "x \<in> T" and "T \<subseteq> S" 

1093 
shows "x \<in> interior S" 

1094 
using assms unfolding interior_def by fast 

1095 

1096 
lemma interiorE [elim?]: 

1097 
assumes "x \<in> interior S" 

1098 
obtains T where "open T" and "x \<in> T" and "T \<subseteq> S" 

1099 
using assms unfolding interior_def by fast 

1100 

1101 
lemma open_interior [simp, intro]: "open (interior S)" 

1102 
by (simp add: interior_def open_Union) 

1103 

1104 
lemma interior_subset: "interior S \<subseteq> S" 

1105 
by (auto simp add: interior_def) 

1106 

1107 
lemma interior_maximal: "T \<subseteq> S \<Longrightarrow> open T \<Longrightarrow> T \<subseteq> interior S" 

1108 
by (auto simp add: interior_def) 

1109 

1110 
lemma interior_open: "open S \<Longrightarrow> interior S = S" 

1111 
by (intro equalityI interior_subset interior_maximal subset_refl) 

33175  1112 

1113 
lemma interior_eq: "interior S = S \<longleftrightarrow> open S" 

44519  1114 
by (metis open_interior interior_open) 
1115 

1116 
lemma open_subset_interior: "open S \<Longrightarrow> S \<subseteq> interior T \<longleftrightarrow> S \<subseteq> T" 

33175  1117 
by (metis interior_maximal interior_subset subset_trans) 
1118 

44519  1119 
lemma interior_empty [simp]: "interior {} = {}" 
1120 
using open_empty by (rule interior_open) 

1121 

44522
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44519
diff
changeset

1122 
lemma interior_UNIV [simp]: "interior UNIV = UNIV" 
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44519
diff
changeset

1123 
using open_UNIV by (rule interior_open) 
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44519
diff
changeset

1124 

44519  1125 
lemma interior_interior [simp]: "interior (interior S) = interior S" 
1126 
using open_interior by (rule interior_open) 

1127 

44522
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44519
diff
changeset

1128 
lemma interior_mono: "S \<subseteq> T \<Longrightarrow> interior S \<subseteq> interior T" 
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44519
diff
changeset

1129 
by (auto simp add: interior_def) 
44519  1130 

1131 
lemma interior_unique: 

1132 
assumes "T \<subseteq> S" and "open T" 

1133 
assumes "\<And>T'. T' \<subseteq> S \<Longrightarrow> open T' \<Longrightarrow> T' \<subseteq> T" 

1134 
shows "interior S = T" 

1135 
by (intro equalityI assms interior_subset open_interior interior_maximal) 

1136 

1137 
lemma interior_inter [simp]: "interior (S \<inter> T) = interior S \<inter> interior T" 

44522
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44519
diff
changeset

1138 
by (intro equalityI Int_mono Int_greatest interior_mono Int_lower1 
44519  1139 
Int_lower2 interior_maximal interior_subset open_Int open_interior) 
1140 

1141 
lemma mem_interior: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. ball x e \<subseteq> S)" 

1142 
using open_contains_ball_eq [where S="interior S"] 

1143 
by (simp add: open_subset_interior) 

33175  1144 

1145 
lemma interior_limit_point [intro]: 

1146 
fixes x :: "'a::perfect_space" 

53255  1147 
assumes x: "x \<in> interior S" 
1148 
shows "x islimpt S" 

44072
5b970711fb39
class perfect_space inherits from topological_space;
huffman
parents:
43338
diff
changeset

1149 
using x islimpt_UNIV [of x] 
5b970711fb39
class perfect_space inherits from topological_space;
huffman
parents:
43338
diff
changeset

1150 
unfolding interior_def islimpt_def 
5b970711fb39
class perfect_space inherits from topological_space;
huffman
parents:
43338
diff
changeset

1151 
apply (clarsimp, rename_tac T T') 
5b970711fb39
class perfect_space inherits from topological_space;
huffman
parents:
43338
diff
changeset

1152 
apply (drule_tac x="T \<inter> T'" in spec) 
5b970711fb39
class perfect_space inherits from t 