author  huffman 
Sat, 20 Aug 2011 06:34:51 0700  
changeset 44342  8321948340ea 
parent 44286  8766839efb1b 
child 44365  5daa55003649 
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 

44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44131
diff
changeset

10 
imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs" 
33175  11 
begin 
12 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
37452
diff
changeset

13 
(* to be moved elsewhere *) 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
37452
diff
changeset

14 

44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
37452
diff
changeset

15 
lemma euclidean_dist_l2:"dist x (y::'a::euclidean_space) = setL2 (\<lambda>i. dist(x$$i) (y$$i)) {..<DIM('a)}" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
37452
diff
changeset

16 
unfolding dist_norm norm_eq_sqrt_inner setL2_def apply(subst euclidean_inner) 
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44252
diff
changeset

17 
apply(auto simp add:power2_eq_square) unfolding euclidean_component_diff .. 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
37452
diff
changeset

18 

44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
37452
diff
changeset

19 
lemma dist_nth_le: "dist (x $$ i) (y $$ i) \<le> dist x (y::'a::euclidean_space)" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
37452
diff
changeset

20 
apply(subst(2) euclidean_dist_l2) apply(cases "i<DIM('a)") 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
37452
diff
changeset

21 
apply(rule member_le_setL2) by auto 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
37452
diff
changeset

22 

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

23 
subsection {* General notion of a topologies as values *} 
33175  24 

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

25 
definition "istopology L \<longleftrightarrow> 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))" 
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

26 
typedef (open) 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}" 
33175  27 
morphisms "openin" "topology" 
28 
unfolding istopology_def by blast 

29 

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

31 
using openin[of U] by blast 

32 

33 
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

34 
using topology_inverse[unfolded mem_Collect_eq] . 
33175  35 

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

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

38 

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

40 
proof 

41 
{assume "T1=T2" hence "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S" by simp} 

42 
moreover 

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

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

44 
hence "openin T1 = openin T2" by (simp add: fun_eq_iff) 
33175  45 
hence "topology (openin T1) = topology (openin T2)" by simp 
46 
hence "T1 = T2" unfolding openin_inverse .} 

47 
ultimately show ?thesis by blast 

48 
qed 

49 

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

51 

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

53 

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

54 
subsubsection {* Main properties of open sets *} 
33175  55 

56 
lemma openin_clauses: 

57 
fixes U :: "'a topology" 

58 
shows "openin U {}" 

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

60 
"\<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

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

62 
by fast+ 
33175  63 

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

65 
unfolding topspace_def by blast 

66 
lemma openin_empty[simp]: "openin U {}" by (simp add: openin_clauses) 

67 

68 
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

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

70 

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

71 
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

72 
using openin_clauses by simp 
33175  73 

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

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

76 

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

78 

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

36584  80 
proof 
81 
assume ?lhs then show ?rhs by auto 

82 
next 

83 
assume H: ?rhs 

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

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

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

87 
finally show "openin U S" . 

33175  88 
qed 
89 

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

90 
subsubsection {* Closed sets *} 
33175  91 

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

93 

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

95 
lemma closedin_empty[simp]: "closedin U {}" by (simp add: closedin_def) 

96 
lemma closedin_topspace[intro,simp]: 

97 
"closedin U (topspace U)" by (simp add: closedin_def) 

98 
lemma closedin_Un[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<union> T)" 

99 
by (auto simp add: Diff_Un closedin_def) 

100 

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

102 
lemma closedin_Inter[intro]: assumes Ke: "K \<noteq> {}" and Kc: "\<forall>S \<in>K. closedin U S" 

103 
shows "closedin U (\<Inter> K)" using Ke Kc unfolding closedin_def Diff_Inter by auto 

104 

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

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

107 

108 
lemma Diff_Diff_Int: "A  (A  B) = A \<inter> B" by blast 

109 
lemma openin_closedin_eq: "openin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> closedin U (topspace U  S)" 

110 
apply (auto simp add: closedin_def Diff_Diff_Int inf_absorb2) 

111 
apply (metis openin_subset subset_eq) 

112 
done 

113 

114 
lemma openin_closedin: "S \<subseteq> topspace U \<Longrightarrow> (openin U S \<longleftrightarrow> closedin U (topspace U  S))" 

115 
by (simp add: openin_closedin_eq) 

116 

117 
lemma openin_diff[intro]: assumes oS: "openin U S" and cT: "closedin U T" shows "openin U (S  T)" 

118 
proof 

119 
have "S  T = S \<inter> (topspace U  T)" using openin_subset[of U S] oS cT 

120 
by (auto simp add: topspace_def openin_subset) 

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

122 
qed 

123 

124 
lemma closedin_diff[intro]: assumes oS: "closedin U S" and cT: "openin U T" shows "closedin U (S  T)" 

125 
proof 

126 
have "S  T = S \<inter> (topspace U  T)" using closedin_subset[of U S] oS cT 

127 
by (auto simp add: topspace_def ) 

128 
then show ?thesis using oS cT by (auto simp add: openin_closedin_eq) 

129 
qed 

130 

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

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

132 

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

133 
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

134 

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

135 
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

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

138 
have "?L {}" by blast 
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

139 
{fix A B assume A: "?L A" and B: "?L B" 
33175  140 
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" by blast 
141 
have "A\<inter>B = (Sa \<inter> Sb) \<inter> V" "openin U (Sa \<inter> Sb)" using Sa Sb by blast+ 

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

142 
then have "?L (A \<inter> B)" by blast} 
33175  143 
moreover 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

144 
{fix K assume K: "K \<subseteq> Collect ?L" 
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

145 
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

146 
apply (rule set_eqI) 
33175  147 
apply (simp add: Ball_def image_iff) 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

148 
by metis 
33175  149 
from K[unfolded th0 subset_image_iff] 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

150 
obtain Sk where Sk: "Sk \<subseteq> Collect (openin U)" "K = (\<lambda>S. S \<inter> V) ` Sk" by blast 
33175  151 
have "\<Union>K = (\<Union>Sk) \<inter> V" using Sk by auto 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

152 
moreover have "openin U (\<Union> Sk)" using Sk by (auto simp add: subset_eq) 
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

153 
ultimately have "?L (\<Union>K)" by blast} 
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

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

155 
unfolding subset_eq mem_Collect_eq istopology_def by blast 
33175  156 
qed 
157 

158 
lemma openin_subtopology: 

159 
"openin (subtopology U V) S \<longleftrightarrow> (\<exists> T. (openin U T) \<and> (S = T \<inter> V))" 

160 
unfolding subtopology_def topology_inverse'[OF istopology_subtopology] 

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

161 
by auto 
33175  162 

163 
lemma topspace_subtopology: "topspace(subtopology U V) = topspace U \<inter> V" 

164 
by (auto simp add: topspace_def openin_subtopology) 

165 

166 
lemma closedin_subtopology: 

167 
"closedin (subtopology U V) S \<longleftrightarrow> (\<exists>T. closedin U T \<and> S = T \<inter> V)" 

168 
unfolding closedin_def topspace_subtopology 

169 
apply (simp add: openin_subtopology) 

170 
apply (rule iffI) 

171 
apply clarify 

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

173 
by auto 

174 

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

176 
unfolding openin_subtopology 

177 
apply (rule iffI, clarify) 

178 
apply (frule openin_subset[of U]) apply blast 

179 
apply (rule exI[where x="topspace U"]) 

180 
by auto 

181 

182 
lemma subtopology_superset: assumes UV: "topspace U \<subseteq> V" 

183 
shows "subtopology U V = U" 

184 
proof 

185 
{fix S 

186 
{fix T assume T: "openin U T" "S = T \<inter> V" 

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

188 
have "openin U S" unfolding eq using T by blast} 

189 
moreover 

190 
{assume S: "openin U S" 

191 
hence "\<exists>T. openin U T \<and> S = T \<inter> V" 

192 
using openin_subset[OF S] UV by auto} 

193 
ultimately have "(\<exists>T. openin U T \<and> S = T \<inter> V) \<longleftrightarrow> openin U S" by blast} 

194 
then show ?thesis unfolding topology_eq openin_subtopology by blast 

195 
qed 

196 

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

198 
by (simp add: subtopology_superset) 

199 

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

201 
by (simp add: subtopology_superset) 

202 

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

203 
subsubsection {* The standard Euclidean topology *} 
33175  204 

205 
definition 

206 
euclidean :: "'a::topological_space topology" where 

207 
"euclidean = topology open" 

208 

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

210 
unfolding euclidean_def 

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

212 
apply (rule topology_inverse[symmetric]) 

213 
apply (auto simp add: istopology_def) 

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

214 
done 
33175  215 

216 
lemma topspace_euclidean: "topspace euclidean = UNIV" 

217 
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

218 
apply (rule set_eqI) 
33175  219 
by (auto simp add: open_openin[symmetric]) 
220 

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

222 
by (simp add: topspace_euclidean topspace_subtopology) 

223 

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

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

226 

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

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

229 

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

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

231 

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

232 
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

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

234 

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

235 
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

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

237 

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

238 
lemma open_openin_trans[trans]: 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

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

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

241 

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

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

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

244 

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

245 
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

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

247 

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

248 
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

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

250 

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

251 
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

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

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

254 
apply (frule closedin_closed_Int[of T S]) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

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

256 

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

257 
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

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

259 

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

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

261 
fixes S U :: "'a::metric_space set" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

262 
shows "openin (subtopology euclidean U) S 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

263 
\<longleftrightarrow> S \<subseteq> U \<and> (\<forall>x\<in>S. \<exists>e>0. \<forall>x'\<in>U. dist x' x < e \<longrightarrow> x'\<in> S)" (is "?lhs \<longleftrightarrow> ?rhs") 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

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

265 
assume ?lhs thus ?rhs unfolding openin_open open_dist by blast 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

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

267 
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

268 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

286 

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

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

288 

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

289 
lemma openin_trans[trans]: "openin (subtopology euclidean T) S \<Longrightarrow> openin (subtopology euclidean U) T 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

290 
\<Longrightarrow> openin (subtopology euclidean U) S" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

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

292 

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

293 
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

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

295 

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

296 
lemma closedin_trans[trans]: 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

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

298 
closedin (subtopology euclidean U) T 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

299 
==> closedin (subtopology euclidean U) S" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

300 
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

301 

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

302 
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

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

304 

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

305 

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

306 
subsection {* Open and closed balls *} 
33175  307 

308 
definition 

309 
ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" where 

310 
"ball x e = {y. dist x y < e}" 

311 

312 
definition 

313 
cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" where 

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

315 

316 
lemma mem_ball[simp]: "y \<in> ball x e \<longleftrightarrow> dist x y < e" by (simp add: ball_def) 

317 
lemma mem_cball[simp]: "y \<in> cball x e \<longleftrightarrow> dist x y \<le> e" by (simp add: cball_def) 

318 

319 
lemma mem_ball_0 [simp]: 

320 
fixes x :: "'a::real_normed_vector" 

321 
shows "x \<in> ball 0 e \<longleftrightarrow> norm x < e" 

322 
by (simp add: dist_norm) 

323 

324 
lemma mem_cball_0 [simp]: 

325 
fixes x :: "'a::real_normed_vector" 

326 
shows "x \<in> cball 0 e \<longleftrightarrow> norm x \<le> e" 

327 
by (simp add: dist_norm) 

328 

329 
lemma centre_in_cball[simp]: "x \<in> cball x e \<longleftrightarrow> 0\<le> e" by simp 

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

331 
lemma subset_ball[intro]: "d <= e ==> ball x d \<subseteq> ball x e" by (simp add: subset_eq) 

332 
lemma subset_cball[intro]: "d <= e ==> cball x d \<subseteq> cball x e" by (simp add: subset_eq) 

333 
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

334 
by (simp add: set_eq_iff) arith 
33175  335 

336 
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

337 
by (simp add: set_eq_iff) 
33175  338 

339 
lemma diff_less_iff: "(a::real)  b > 0 \<longleftrightarrow> a > b" 

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

341 
"a  b < c \<longleftrightarrow> a < c +b" "a  b > c \<longleftrightarrow> a > c +b" by arith+ 

342 
lemma diff_le_iff: "(a::real)  b \<ge> 0 \<longleftrightarrow> a \<ge> b" "(a::real)  b \<le> 0 \<longleftrightarrow> a \<le> b" 

343 
"a  b \<le> c \<longleftrightarrow> a \<le> c +b" "a  b \<ge> c \<longleftrightarrow> a \<ge> c +b" by arith+ 

344 

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

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

346 
unfolding open_dist ball_def mem_Collect_eq Ball_def 
33175  347 
unfolding dist_commute 
348 
apply clarify 

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

350 
using dist_triangle_alt[where z=x] 

351 
apply (clarsimp simp add: diff_less_iff) 

352 
apply atomize 

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

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

355 
by arith 

356 

357 
lemma centre_in_ball[simp]: "x \<in> ball x e \<longleftrightarrow> e > 0" by (metis mem_ball dist_self) 

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

359 
unfolding open_dist subset_eq mem_ball Ball_def dist_commute .. 

360 

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

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

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

363 
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

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

365 

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

368 

369 
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

370 
unfolding mem_ball set_eq_iff 
33175  371 
apply (simp add: not_less) 
372 
by (metis zero_le_dist order_trans dist_self) 

373 

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

375 

376 

377 
subsection{* Connectedness *} 

378 

379 
definition "connected S \<longleftrightarrow> 

380 
~(\<exists>e1 e2. open e1 \<and> open e2 \<and> S \<subseteq> (e1 \<union> e2) \<and> (e1 \<inter> e2 \<inter> S = {}) 

381 
\<and> ~(e1 \<inter> S = {}) \<and> ~(e2 \<inter> S = {}))" 

382 

383 
lemma connected_local: 

384 
"connected S \<longleftrightarrow> ~(\<exists>e1 e2. 

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

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

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

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

389 
~(e1 = {}) \<and> 

390 
~(e2 = {}))" 

391 
unfolding connected_def openin_open by (safe, blast+) 

392 

34105  393 
lemma exists_diff: 
394 
fixes P :: "'a set \<Rightarrow> bool" 

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

33175  396 
proof 
397 
{assume "?lhs" hence ?rhs by blast } 

398 
moreover 

399 
{fix S assume H: "P S" 

34105  400 
have "S =  ( S)" by auto 
401 
with H have "P ( ( S))" by metis } 

33175  402 
ultimately show ?thesis by metis 
403 
qed 

404 

405 
lemma connected_clopen: "connected S \<longleftrightarrow> 

406 
(\<forall>T. openin (subtopology euclidean S) T \<and> 

407 
closedin (subtopology euclidean S) T \<longrightarrow> T = {} \<or> T = S)" (is "?lhs \<longleftrightarrow> ?rhs") 

408 
proof 

34105  409 
have " \<not> connected S \<longleftrightarrow> (\<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  410 
unfolding connected_def openin_open closedin_closed 
411 
apply (subst exists_diff) by blast 

34105  412 
hence th0: "connected S \<longleftrightarrow> \<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> {})" 
413 
(is " _ \<longleftrightarrow> \<not> (\<exists>e2 e1. ?P e2 e1)") apply (simp add: closed_def) by metis 

33175  414 

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

416 
(is "_ \<longleftrightarrow> \<not> (\<exists>t' t. ?Q t' t)") 

417 
unfolding connected_def openin_open closedin_closed by auto 

418 
{fix e2 

419 
{fix e1 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)" 

420 
by auto} 

421 
then have "(\<exists>e1. ?P e2 e1) \<longleftrightarrow> (\<exists>t. ?Q e2 t)" by metis} 

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

423 
then show ?thesis unfolding th0 th1 by simp 

424 
qed 

425 

426 
lemma connected_empty[simp, intro]: "connected {}" 

427 
by (simp add: connected_def) 

428 

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

429 

33175  430 
subsection{* Limit points *} 
431 

44207
ea99698c2070
localeize some definitions, so perfect_space and heine_borel can inherit from the proper superclasses
huffman
parents:
44170
diff
changeset

432 
definition (in topological_space) 
ea99698c2070
localeize some definitions, so perfect_space and heine_borel can inherit from the proper superclasses
huffman
parents:
44170
diff
changeset

433 
islimpt:: "'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "islimpt" 60) where 
33175  434 
"x islimpt S \<longleftrightarrow> (\<forall>T. x\<in>T \<longrightarrow> open T \<longrightarrow> (\<exists>y\<in>S. y\<in>T \<and> y\<noteq>x))" 
435 

436 
lemma islimptI: 

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

438 
shows "x islimpt S" 

439 
using assms unfolding islimpt_def by auto 

440 

441 
lemma islimptE: 

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

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

444 
using assms unfolding islimpt_def by auto 

445 

446 
lemma islimpt_subset: "x islimpt S \<Longrightarrow> S \<subseteq> T ==> x islimpt T" by (auto simp add: islimpt_def) 

447 

448 
lemma islimpt_approachable: 

449 
fixes x :: "'a::metric_space" 

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

451 
unfolding islimpt_def 

452 
apply auto 

453 
apply(erule_tac x="ball x e" in allE) 

454 
apply auto 

455 
apply(rule_tac x=y in bexI) 

456 
apply (auto simp add: dist_commute) 

457 
apply (simp add: open_dist, drule (1) bspec) 

458 
apply (clarify, drule spec, drule (1) mp, auto) 

459 
done 

460 

461 
lemma islimpt_approachable_le: 

462 
fixes x :: "'a::metric_space" 

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

464 
unfolding islimpt_approachable 

465 
using approachable_lt_le[where f="\<lambda>x'. dist x' x" and P="\<lambda>x'. \<not> (x'\<in>S \<and> x'\<noteq>x)"] 

33324  466 
by metis 
33175  467 

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

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

469 

44207
ea99698c2070
localeize some definitions, so perfect_space and heine_borel can inherit from the proper superclasses
huffman
parents:
44170
diff
changeset

470 
class perfect_space = topological_space + 
ea99698c2070
localeize some definitions, so perfect_space and heine_borel can inherit from the proper superclasses
huffman
parents:
44170
diff
changeset

471 
assumes islimpt_UNIV [simp, intro]: "x islimpt UNIV" 
33175  472 

473 
lemma perfect_choose_dist: 

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

474 
fixes x :: "'a::{perfect_space, metric_space}" 
33175  475 
shows "0 < r \<Longrightarrow> \<exists>a. a \<noteq> x \<and> dist a x < r" 
476 
using islimpt_UNIV [of x] 

477 
by (simp add: islimpt_approachable) 

478 

44129  479 
instance euclidean_space \<subseteq> perfect_space 
44122  480 
proof 
481 
fix x :: 'a 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
37452
diff
changeset

482 
{ fix e :: real assume "0 < e" 
44122  483 
def y \<equiv> "x + scaleR (e/2) (sgn (basis 0))" 
484 
from `0 < e` have "y \<noteq> x" 

44167  485 
unfolding y_def by (simp add: sgn_zero_iff DIM_positive) 
44122  486 
from `0 < e` have "dist y x < e" 
487 
unfolding y_def by (simp add: dist_norm norm_sgn) 

33175  488 
from `y \<noteq> x` and `dist y x < e` 
489 
have "\<exists>y\<in>UNIV. y \<noteq> x \<and> dist y x < e" by auto 

490 
} 

491 
then show "x islimpt UNIV" unfolding islimpt_approachable by blast 

492 
qed 

493 

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

495 
unfolding closed_def 

496 
apply (subst open_subopen) 

34105  497 
apply (simp add: islimpt_def subset_eq) 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

498 
by (metis ComplE ComplI) 
33175  499 

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

501 
unfolding islimpt_def by auto 

502 

503 
lemma finite_set_avoid: 

504 
fixes a :: "'a::metric_space" 

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

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

41863  507 
case 1 thus ?case by (auto intro: zero_less_one) 
33175  508 
next 
509 
case (2 x F) 

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

511 
{assume "x = a" hence ?case using d by auto } 

512 
moreover 

513 
{assume xa: "x\<noteq>a" 

514 
let ?d = "min d (dist a x)" 

515 
have dp: "?d > 0" using xa d(1) using dist_nz by auto 

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

517 
with dp xa have ?case by(auto intro!: exI[where x="?d"]) } 

518 
ultimately show ?case by blast 

519 
qed 

520 

521 
lemma islimpt_finite: 

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

523 
assumes fS: "finite S" shows "\<not> a islimpt S" 

524 
unfolding islimpt_approachable 

525 
using finite_set_avoid[OF fS, of a] by (metis dist_commute not_le) 

526 

527 
lemma islimpt_Un: "x islimpt (S \<union> T) \<longleftrightarrow> x islimpt S \<or> x islimpt T" 

528 
apply (rule iffI) 

529 
defer 

530 
apply (metis Un_upper1 Un_upper2 islimpt_subset) 

531 
unfolding islimpt_def 

532 
apply (rule ccontr, clarsimp, rename_tac A B) 

533 
apply (drule_tac x="A \<inter> B" in spec) 

534 
apply (auto simp add: open_Int) 

535 
done 

536 

537 
lemma discrete_imp_closed: 

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

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

540 
shows "closed S" 

541 
proof 

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

543 
from e have e2: "e/2 > 0" by arith 

544 
from C[rule_format, OF e2] obtain y where y: "y \<in> S" "y\<noteq>x" "dist y x < e/2" by blast 

545 
let ?m = "min (e/2) (dist x y) " 

546 
from e2 y(2) have mp: "?m > 0" by (simp add: dist_nz[THEN sym]) 

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

548 
have th: "dist z y < e" using z y 

549 
by (intro dist_triangle_lt [where z=x], simp) 

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

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

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

553 
qed 

554 

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

555 

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

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

557 

33175  558 
definition "interior S = {x. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S}" 
559 

560 
lemma interior_eq: "interior S = S \<longleftrightarrow> open 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

561 
apply (simp add: set_eq_iff interior_def) 
33175  562 
apply (subst (2) open_subopen) by (safe, blast+) 
563 

564 
lemma interior_open: "open S ==> (interior S = S)" by (metis interior_eq) 

565 

566 
lemma interior_empty[simp]: "interior {} = {}" by (simp add: interior_def) 

567 

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

569 
apply (simp add: interior_def) 

570 
apply (subst open_subopen) by blast 

571 

572 
lemma interior_interior[simp]: "interior(interior S) = interior S" by (metis interior_eq open_interior) 

573 
lemma interior_subset: "interior S \<subseteq> S" by (auto simp add: interior_def) 

574 
lemma subset_interior: "S \<subseteq> T ==> (interior S) \<subseteq> (interior T)" by (auto simp add: interior_def) 

575 
lemma interior_maximal: "T \<subseteq> S \<Longrightarrow> open T ==> T \<subseteq> (interior S)" by (auto simp add: interior_def) 

576 
lemma interior_unique: "T \<subseteq> S \<Longrightarrow> open T \<Longrightarrow> (\<forall>T'. T' \<subseteq> S \<and> open T' \<longrightarrow> T' \<subseteq> T) \<Longrightarrow> interior S = T" 

577 
by (metis equalityI interior_maximal interior_subset open_interior) 

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

579 
apply (simp add: interior_def) 

580 
by (metis open_contains_ball centre_in_ball open_ball subset_trans) 

581 

582 
lemma open_subset_interior: "open S ==> S \<subseteq> interior T \<longleftrightarrow> S \<subseteq> T" 

583 
by (metis interior_maximal interior_subset subset_trans) 

584 

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

586 
apply (rule equalityI, simp) 

587 
apply (metis Int_lower1 Int_lower2 subset_interior) 

588 
by (metis Int_mono interior_subset open_Int open_interior open_subset_interior) 

589 

590 
lemma interior_limit_point [intro]: 

591 
fixes x :: "'a::perfect_space" 

592 
assumes x: "x \<in> interior S" shows "x islimpt S" 

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

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

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

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

596 
apply (drule_tac x="T \<inter> T'" in spec) 
5b970711fb39
class perfect_space inherits from topological_space;
huffman
parents:
43338
diff
changeset

597 
apply (auto simp add: open_Int) 
5b970711fb39
class perfect_space inherits from topological_space;
huffman
parents:
43338
diff
changeset

598 
done 
33175  599 

600 
lemma interior_closed_Un_empty_interior: 

601 
assumes cS: "closed S" and iT: "interior T = {}" 

602 
shows "interior(S \<union> T) = interior S" 

603 
proof 

604 
show "interior S \<subseteq> interior (S\<union>T)" 

605 
by (rule subset_interior, blast) 

606 
next 

607 
show "interior (S \<union> T) \<subseteq> interior S" 

608 
proof 

609 
fix x assume "x \<in> interior (S \<union> T)" 

610 
then obtain R where "open R" "x \<in> R" "R \<subseteq> S \<union> T" 

611 
unfolding interior_def by fast 

612 
show "x \<in> interior S" 

613 
proof (rule ccontr) 

614 
assume "x \<notin> interior S" 

615 
with `x \<in> R` `open R` obtain y where "y \<in> R  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

616 
unfolding interior_def set_eq_iff by fast 
33175  617 
from `open R` `closed S` have "open (R  S)" by (rule open_Diff) 
618 
from `R \<subseteq> S \<union> T` have "R  S \<subseteq> T" by fast 

619 
from `y \<in> R  S` `open (R  S)` `R  S \<subseteq> T` `interior T = {}` 

620 
show "False" unfolding interior_def by fast 

621 
qed 

622 
qed 

623 
qed 

624 

625 

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

626 
subsection {* Closure of a Set *} 
33175  627 

628 
definition "closure S = S \<union> {x  x. x islimpt S}" 

629 

34105  630 
lemma closure_interior: "closure S =  interior ( S)" 
33175  631 
proof 
632 
{ fix x 

34105  633 
have "x\<in> interior ( S) \<longleftrightarrow> x \<in> closure S" (is "?lhs = ?rhs") 
33175  634 
proof 
34105  635 
let ?exT = "\<lambda> y. (\<exists>T. open T \<and> y \<in> T \<and> T \<subseteq>  S)" 
33175  636 
assume "?lhs" 
637 
hence *:"\<not> ?exT x" 

638 
unfolding interior_def 

639 
by simp 

640 
{ assume "\<not> ?rhs" 

641 
hence False using * 

642 
unfolding closure_def islimpt_def 

643 
by blast 

644 
} 

645 
thus "?rhs" 

646 
by blast 

647 
next 

648 
assume "?rhs" thus "?lhs" 

649 
unfolding closure_def interior_def islimpt_def 

650 
by blast 

651 
qed 

652 
} 

653 
thus ?thesis 

654 
by blast 

655 
qed 

656 

34105  657 
lemma interior_closure: "interior S =  (closure ( S))" 
33175  658 
proof 
659 
{ fix x 

34105  660 
have "x \<in> interior S \<longleftrightarrow> x \<in>  (closure ( S))" 
33175  661 
unfolding interior_def closure_def islimpt_def 
33324  662 
by auto 
33175  663 
} 
664 
thus ?thesis 

665 
by blast 

666 
qed 

667 

668 
lemma closed_closure[simp, intro]: "closed (closure S)" 

669 
proof 

34105  670 
have "closed ( interior (S))" by blast 
33175  671 
thus ?thesis using closure_interior[of S] by simp 
672 
qed 

673 

674 
lemma closure_hull: "closure S = closed hull S" 

675 
proof 

676 
have "S \<subseteq> closure S" 

677 
unfolding closure_def 

678 
by blast 

679 
moreover 

680 
have "closed (closure S)" 

681 
using closed_closure[of S] 

682 
by assumption 

683 
moreover 

684 
{ fix t 

685 
assume *:"S \<subseteq> t" "closed t" 

686 
{ fix x 

687 
assume "x islimpt S" 

688 
hence "x islimpt t" using *(1) 

689 
using islimpt_subset[of x, of S, of t] 

690 
by blast 

691 
} 

692 
with * have "closure S \<subseteq> t" 

693 
unfolding closure_def 

694 
using closed_limpt[of t] 

695 
by auto 

696 
} 

697 
ultimately show ?thesis 

698 
using hull_unique[of S, of "closure S", of closed] 

699 
by simp 

700 
qed 

701 

702 
lemma closure_eq: "closure S = S \<longleftrightarrow> closed S" 

703 
unfolding closure_hull 

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

704 
using hull_eq[of closed, OF closed_Inter, of S] 
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

705 
by metis 
33175  706 

707 
lemma closure_closed[simp]: "closed S \<Longrightarrow> closure S = S" 

708 
using closure_eq[of S] 

709 
by simp 

710 

711 
lemma closure_closure[simp]: "closure (closure S) = closure S" 

712 
unfolding closure_hull 

713 
using hull_hull[of closed S] 

714 
by assumption 

715 

716 
lemma closure_subset: "S \<subseteq> closure S" 

717 
unfolding closure_hull 

718 
using hull_subset[of S closed] 

719 
by assumption 

720 

721 
lemma subset_closure: "S \<subseteq> T \<Longrightarrow> closure S \<subseteq> closure T" 

722 
unfolding closure_hull 

723 
using hull_mono[of S T closed] 

724 
by assumption 

725 

726 
lemma closure_minimal: "S \<subseteq> T \<Longrightarrow> closed T \<Longrightarrow> closure S \<subseteq> T" 

727 
using hull_minimal[of S T closed] 

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

728 
unfolding closure_hull 
33175  729 
by simp 
730 

731 
lemma closure_unique: "S \<subseteq> T \<and> closed T \<and> (\<forall> T'. S \<subseteq> T' \<and> closed T' \<longrightarrow> T \<subseteq> T') \<Longrightarrow> closure S = T" 

732 
using hull_unique[of S T closed] 

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

733 
unfolding closure_hull 
33175  734 
by simp 
735 

736 
lemma closure_empty[simp]: "closure {} = {}" 

737 
using closed_empty closure_closed[of "{}"] 

738 
by simp 

739 

740 
lemma closure_univ[simp]: "closure UNIV = UNIV" 

741 
using closure_closed[of UNIV] 

742 
by simp 

743 

744 
lemma closure_eq_empty: "closure S = {} \<longleftrightarrow> S = {}" 

745 
using closure_empty closure_subset[of S] 

746 
by blast 

747 

748 
lemma closure_subset_eq: "closure S \<subseteq> S \<longleftrightarrow> closed S" 

749 
using closure_eq[of S] closure_subset[of S] 

750 
by simp 

751 

752 
lemma open_inter_closure_eq_empty: 

753 
"open S \<Longrightarrow> (S \<inter> closure T) = {} \<longleftrightarrow> S \<inter> T = {}" 

34105  754 
using open_subset_interior[of S " T"] 
755 
using interior_subset[of " T"] 

33175  756 
unfolding closure_interior 
757 
by auto 

758 

759 
lemma open_inter_closure_subset: 

760 
"open S \<Longrightarrow> (S \<inter> (closure T)) \<subseteq> closure(S \<inter> T)" 

761 
proof 

762 
fix x 

763 
assume as: "open S" "x \<in> S \<inter> closure T" 

764 
{ assume *:"x islimpt T" 

765 
have "x islimpt (S \<inter> T)" 

766 
proof (rule islimptI) 

767 
fix A 

768 
assume "x \<in> A" "open A" 

769 
with as have "x \<in> A \<inter> S" "open (A \<inter> S)" 

770 
by (simp_all add: open_Int) 

771 
with * obtain y where "y \<in> T" "y \<in> A \<inter> S" "y \<noteq> x" 

772 
by (rule islimptE) 

773 
hence "y \<in> S \<inter> T" "y \<in> A \<and> y \<noteq> x" 

774 
by simp_all 

775 
thus "\<exists>y\<in>(S \<inter> T). y \<in> A \<and> y \<noteq> x" .. 

776 
qed 

777 
} 

778 
then show "x \<in> closure (S \<inter> T)" using as 

779 
unfolding closure_def 

780 
by blast 

781 
qed 

782 

34105  783 
lemma closure_complement: "closure( S) =  interior(S)" 
33175  784 
proof 
34105  785 
have "S =  ( S)" 
33175  786 
by auto 
787 
thus ?thesis 

788 
unfolding closure_interior 

789 
by auto 

790 
qed 

791 

34105  792 
lemma interior_complement: "interior( S) =  closure(S)" 
33175  793 
unfolding closure_interior 
794 
by blast 

795 

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

796 

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

797 
subsection {* Frontier (aka boundary) *} 
33175  798 

799 
definition "frontier S = closure S  interior S" 

800 

801 
lemma frontier_closed: "closed(frontier S)" 

802 
by (simp add: frontier_def closed_Diff) 

803 

34105  804 
lemma frontier_closures: "frontier S = (closure S) \<inter> (closure( S))" 
33175  805 
by (auto simp add: frontier_def interior_closure) 
806 

807 
lemma frontier_straddle: 

808 
fixes a :: "'a::metric_space" 

809 
shows "a \<in> frontier S \<longleftrightarrow> (\<forall>e>0. (\<exists>x\<in>S. dist a x < e) \<and> (\<exists>x. x \<notin> S \<and> dist a x < e))" (is "?lhs \<longleftrightarrow> ?rhs") 

810 
proof 

811 
assume "?lhs" 

812 
{ fix e::real 

813 
assume "e > 0" 

814 
let ?rhse = "(\<exists>x\<in>S. dist a x < e) \<and> (\<exists>x. x \<notin> S \<and> dist a x < e)" 

815 
{ assume "a\<in>S" 

816 
have "\<exists>x\<in>S. dist a x < e" using `e>0` `a\<in>S` by(rule_tac x=a in bexI) auto 

817 
moreover have "\<exists>x. x \<notin> S \<and> dist a x < e" using `?lhs` `a\<in>S` 

818 
unfolding frontier_closures closure_def islimpt_def using `e>0` 

819 
by (auto, erule_tac x="ball a e" in allE, auto) 

820 
ultimately have ?rhse by auto 

821 
} 

822 
moreover 

823 
{ assume "a\<notin>S" 

824 
hence ?rhse using `?lhs` 

825 
unfolding frontier_closures closure_def islimpt_def 

826 
using open_ball[of a e] `e > 0` 

33324  827 
by simp (metis centre_in_ball mem_ball open_ball) 
33175  828 
} 
829 
ultimately have ?rhse by auto 

830 
} 

831 
thus ?rhs by auto 

832 
next 

833 
assume ?rhs 

834 
moreover 

835 
{ fix T assume "a\<notin>S" and 

836 
as:"\<forall>e>0. (\<exists>x\<in>S. dist a x < e) \<and> (\<exists>x. x \<notin> S \<and> dist a x < e)" "a \<notin> S" "a \<in> T" "open T" 

837 
from `open T` `a \<in> T` have "\<exists>e>0. ball a e \<subseteq> T" unfolding open_contains_ball[of T] by auto 

838 
then obtain e where "e>0" "ball a e \<subseteq> T" by auto 

839 
then obtain y where y:"y\<in>S" "dist a y < e" using as(1) by auto 

840 
have "\<exists>y\<in>S. y \<in> T \<and> y \<noteq> a" 

841 
using `dist a y < e` `ball a e \<subseteq> T` unfolding ball_def using `y\<in>S` `a\<notin>S` by auto 

842 
} 

843 
hence "a \<in> closure S" unfolding closure_def islimpt_def using `?rhs` by auto 

844 
moreover 

845 
{ fix T assume "a \<in> T" "open T" "a\<in>S" 

846 
then obtain e where "e>0" and balle: "ball a e \<subseteq> T" unfolding open_contains_ball using `?rhs` by auto 

847 
obtain x where "x \<notin> S" "dist a x < e" using `?rhs` using `e>0` by auto 

34105  848 
hence "\<exists>y\<in> S. y \<in> T \<and> y \<noteq> a" using balle `a\<in>S` unfolding ball_def by (rule_tac x=x in bexI)auto 
33175  849 
} 
34105  850 
hence "a islimpt ( S) \<or> a\<notin>S" unfolding islimpt_def by auto 
851 
ultimately show ?lhs unfolding frontier_closures using closure_def[of " S"] by auto 

33175  852 
qed 
853 

854 
lemma frontier_subset_closed: "closed S \<Longrightarrow> frontier S \<subseteq> S" 

855 
by (metis frontier_def closure_closed Diff_subset) 

856 

34964  857 
lemma frontier_empty[simp]: "frontier {} = {}" 
36362
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
36360
diff
changeset

858 
by (simp add: frontier_def) 
33175  859 

860 
lemma frontier_subset_eq: "frontier S \<subseteq> S \<longleftrightarrow> closed S" 

861 
proof 

862 
{ assume "frontier S \<subseteq> S" 

863 
hence "closure S \<subseteq> S" using interior_subset unfolding frontier_def by auto 

864 
hence "closed S" using closure_subset_eq by auto 

865 
} 

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

866 
thus ?thesis using frontier_subset_closed[of S] .. 
33175  867 
qed 
868 

34105  869 
lemma frontier_complement: "frontier( S) = frontier S" 
33175  870 
by (auto simp add: frontier_def closure_complement interior_complement) 
871 

872 
lemma frontier_disjoint_eq: "frontier S \<inter> S = {} \<longleftrightarrow> open S" 

34105  873 
using frontier_complement frontier_subset_eq[of " S"] 
874 
unfolding open_closed by auto 

33175  875 

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

876 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44076
diff
changeset

877 
subsection {* Filters and the ``eventually true'' quantifier *} 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44076
diff
changeset

878 

33175  879 
definition 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44076
diff
changeset

880 
at_infinity :: "'a::real_normed_vector filter" where 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44076
diff
changeset

881 
"at_infinity = Abs_filter (\<lambda>P. \<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x)" 
33175  882 

883 
definition 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44076
diff
changeset

884 
indirection :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> 'a filter" 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44076
diff
changeset

885 
(infixr "indirection" 70) where 
33175  886 
"a indirection v = (at a) within {b. \<exists>c\<ge>0. b  a = scaleR c v}" 
887 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44076
diff
changeset

888 
text{* Prove That They are all filters. *} 
33175  889 

36358
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
36336
diff
changeset

890 
lemma eventually_at_infinity: 
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
36336
diff
changeset

891 
"eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. norm x >= b \<longrightarrow> P x)" 
33175  892 
unfolding at_infinity_def 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44076
diff
changeset

893 
proof (rule eventually_Abs_filter, rule is_filter.intro) 
36358
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
36336
diff
changeset

894 
fix P Q :: "'a \<Rightarrow> bool" 
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
36336
diff
changeset

895 
assume "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x" and "\<exists>s. \<forall>x. s \<le> norm x \<longrightarrow> Q x" 
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
36336
diff
changeset

896 
then obtain r s where 
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
36336
diff
changeset

897 
"\<forall>x. r \<le> norm x \<longrightarrow> P x" and "\<forall>x. s \<le> norm x \<longrightarrow> Q x" by auto 
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
36336
diff
changeset

898 
then have "\<forall>x. max r s \<le> norm x \<longrightarrow> P x \<and> Q x" by simp 
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
36336
diff
changeset

899 
then show "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x \<and> Q x" .. 
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
36336
diff
changeset

900 
qed auto 
33175  901 

36437  902 
text {* Identify Trivial limits, where we can't approach arbitrarily closely. *} 
33175  903 

904 
lemma trivial_limit_within: 

905 
shows "trivial_limit (at a within S) \<longleftrightarrow> \<not> a islimpt S" 

906 
proof 

907 
assume "trivial_limit (at a within S)" 

908 
thus "\<not> a islimpt S" 

909 
unfolding trivial_limit_def 

36358
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
36336
diff
changeset

910 
unfolding eventually_within eventually_at_topological 
33175  911 
unfolding islimpt_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

912 
apply (clarsimp simp add: set_eq_iff) 
33175  913 
apply (rename_tac T, rule_tac x=T in exI) 
36358
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
36336
diff
changeset

914 
apply (clarsimp, drule_tac x=y in bspec, simp_all) 
33175  915 
done 
916 
next 

917 
assume "\<not> a islimpt S" 

918 
thus "trivial_limit (at a within S)" 

919 
unfolding trivial_limit_def 

36358
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
36336
diff
changeset

920 
unfolding eventually_within eventually_at_topological 
33175  921 
unfolding islimpt_def 
36358
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
36336
diff
changeset

922 
apply clarsimp 
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
36336
diff
changeset

923 
apply (rule_tac x=T in exI) 
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
36336
diff
changeset

924 
apply auto 
33175  925 
done 
926 
qed 

927 

928 
lemma trivial_limit_at_iff: "trivial_limit (at a) \<longleftrightarrow> \<not> a islimpt UNIV" 

929 
using trivial_limit_within [of a UNIV] 

930 
by (simp add: within_UNIV) 

931 

932 
lemma trivial_limit_at: 

933 
fixes a :: "'a::perfect_space" 

934 
shows "\<not> trivial_limit (at a)" 

935 
by (simp add: trivial_limit_at_iff) 

936 

937 
lemma trivial_limit_at_infinity: 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44076
diff
changeset

938 
"\<not> trivial_limit (at_infinity :: ('a::{real_normed_vector,perfect_space}) filter)" 
36358
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
36336
diff
changeset

939 
unfolding trivial_limit_def eventually_at_infinity 
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
36336
diff
changeset

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

941 
apply (subgoal_tac "\<exists>x::'a. x \<noteq> 0", clarify) 
5b970711fb39
class perfect_space inherits from topological_space;
huffman
parents:
43338
diff
changeset

942 
apply (rule_tac x="scaleR (b / norm x) x" in exI, simp) 
5b970711fb39
class perfect_space inherits from topological_space;
huffman
parents:
43338
diff
changeset

943 
apply (cut_tac islimpt_UNIV [of "0::'a", unfolded islimpt_def]) 
5b970711fb39
class perfect_space inherits from topological_space;
huffman
parents:
43338
diff
changeset

944 
apply (drule_tac x=UNIV in spec, simp) 
33175  945 
done 
946 

36437  947 
text {* Some property holds "sufficiently close" to the limit point. *} 
33175  948 

949 
lemma eventually_at: (* FIXME: this replaces Limits.eventually_at *) 

950 
"eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)" 

951 
unfolding eventually_at dist_nz by auto 

952 

953 
lemma eventually_within: "eventually P (at a within S) \<longleftrightarrow> 

954 
(\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)" 

955 
unfolding eventually_within eventually_at dist_nz by auto 

956 

957 
lemma eventually_within_le: "eventually P (at a within S) \<longleftrightarrow> 

958 
(\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a <= d \<longrightarrow> P x)" (is "?lhs = ?rhs") 

959 
unfolding eventually_within 

33324  960 
by auto (metis Rats_dense_in_nn_real order_le_less_trans order_refl) 
33175  961 

962 
lemma eventually_happens: "eventually P net ==> trivial_limit net \<or> (\<exists>x. P x)" 

36358
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
36336
diff
changeset

963 
unfolding trivial_limit_def 
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
36336
diff
changeset

964 
by (auto elim: eventually_rev_mp) 
33175  965 

966 
lemma trivial_limit_eventually: "trivial_limit net \<Longrightarrow> eventually P net" 

36358
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
36336
diff
changeset

967 
unfolding trivial_limit_def by (auto elim: eventually_rev_mp) 
33175  968 

969 
lemma trivial_limit_eq: "trivial_limit net \<longleftrightarrow> (\<forall>P. eventually P net)" 

44342
8321948340ea
redefine constant 'trivial_limit' as an abbreviation
huffman
parents:
44286
diff
changeset

970 
by (simp add: filter_eq_iff) 
33175  971 

972 
text{* Combining theorems for "eventually" *} 

973 

974 
lemma eventually_rev_mono: 

975 
"eventually P net \<Longrightarrow> (\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually Q net" 

976 
using eventually_mono [of P Q] by fast 

977 

978 
lemma not_eventually: "(\<forall>x. \<not> P x ) \<Longrightarrow> ~(trivial_limit net) ==> ~(eventually (\<lambda>x. P x) net)" 

979 
by (simp add: eventually_False) 

980 

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

981 

36437  982 
subsection {* Limits *} 
33175  983 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44076
diff
changeset

984 
text{* Notation Lim to avoid collition with lim defined in analysis *} 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44076
diff
changeset

985 

730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44076
diff
changeset

986 
definition Lim :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b::t2_space) \<Rightarrow> 'b" 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44076
diff
changeset

987 
where "Lim A f = (THE l. (f > l) A)" 
33175  988 

989 
lemma Lim: 

990 
"(f > l) net \<longleftrightarrow> 

991 
trivial_limit net \<or> 

992 
(\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)" 

993 
unfolding tendsto_iff trivial_limit_eq by auto 

994 

995 
text{* Show that they yield usual definitions in the various cases. *} 

996 

997 
lemma Lim_within_le: "(f > l)(at a within S) \<longleftrightarrow> 

998 
(\<forall>e>0. \<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a <= d \<longrightarrow> dist (f x) l < e)" 

999 
by (auto simp add: tendsto_iff eventually_within_le) 

1000 

1001 
lemma Lim_within: "(f > l) (at a within S) \<longleftrightarrow> 

1002 
(\<forall>e >0. \<exists>d>0. \<forall>x \<in> S. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e)" 

1003 
by (auto simp add: tendsto_iff eventually_within) 

1004 

1005 
lemma Lim_at: "(f > l) (at a) \<longleftrightarrow> 

1006 
(\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e)" 

1007 
by (auto simp add: tendsto_iff eventually_at) 

1008 

1009 
lemma Lim_at_iff_LIM: "(f > l) (at a) \<longleftrightarrow> f  a > l" 

1010 
unfolding Lim_at LIM_def by (simp only: zero_less_dist_iff) 

1011 

1012 
lemma Lim_at_infinity: 

1013 
"(f > l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x >= b \<longrightarrow> dist (f x) l < e)" 

1014 
by (auto simp add: tendsto_iff eventually_at_infinity) 

1015 

1016 
lemma Lim_sequentially: 

1017 
"(S > l) sequentially \<longleftrightarrow> 

1018 
(\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (S n) l < e)" 

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

1019 
by (rule LIMSEQ_def) (* FIXME: redundant *) 
33175  1020 

1021 
lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f > l) net" 

1022 
by (rule topological_tendstoI, auto elim: eventually_rev_mono) 

1023 

1024 
text{* The expected monotonicity property. *} 

1025 

1026 
lemma Lim_within_empty: "(f > l) (net within {})" 

1027 
unfolding tendsto_def Limits.eventually_within by simp 

1028 

1029 
lemma Lim_within_subset: "(f > l) (net within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f > l) (net within T)" 

1030 
unfolding tendsto_def Limits.eventually_within 

1031 
by (auto elim!: eventually_elim1) 

1032 

1033 
lemma Lim_Un: assumes "(f > l) (net within S)" "(f > l) (net within T)" 

1034 
shows "(f > l) (net within (S \<union> T))" 

1035 
using assms unfolding tendsto_def Limits.eventually_within 

1036 
apply clarify 

1037 
apply (drule spec, drule (1) mp, drule (1) mp) 

1038 
apply (drule spec, drule (1) mp, drule (1) mp) 

1039 
apply (auto elim: eventually_elim2) 

1040 
done 

1041 

1042 
lemma Lim_Un_univ: 

1043 
"(f > l) (net within S) \<Longrightarrow> (f > l) (net within T) \<Longrightarrow> S \<union> T = UNIV 

1044 
==> (f > l) net" 

1045 
by (metis Lim_Un within_UNIV) 

1046 

1047 
text{* Interrelations between restricted and unrestricted limits. *} 

1048 

1049 
lemma Lim_at_within: "(f > l) net ==> (f > l)(net within S)" 

1050 
(* FIXME: rename *) 

1051 
unfolding tendsto_def Limits.eventually_within 

1052 
apply (clarify, drule spec, drule (1) mp, drule (1) mp) 

1053 
by (auto elim!: eventually_elim1) 

1054 

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

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

1056 
assumes "x \<in> interior S" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

1057 
shows "eventually P (at x within S) \<longleftrightarrow> eventually P (at x)" (is "?lhs = ?rhs") 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

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

1059 
from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

1060 
unfolding interior_def by fast 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

1061 
{ assume "?lhs" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

1062 
then obtain A where "open A" "x \<in> A" "\<forall>y\<in>A. y \<noteq> x \<longrightarrow> y \<in> S \<longrightarrow> P y" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

1063 
unfolding Limits.eventually_within Limits.eventually_at_topological 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

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

1065 
with T have "open (A \<inter> T)" "x \<in> A \<inter> T" "\<forall>y\<in>(A \<inter> T). y \<noteq> x \<longrightarrow> P y" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

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

1067 
then have "?rhs" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

1068 
unfolding Limits.eventually_at_topological by auto 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

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

1070 
{ assume "?rhs" hence "?lhs" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

1071 
unfolding Limits.eventually_within 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

1072 
by (auto elim: eventually_elim1) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

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

1074 
show "?thesis" .. 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

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

1076 

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

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

1078 
"x \<in> interior S \<Longrightarrow> at x within S = at x" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

1079 
by (simp add: filter_eq_iff eventually_within_interior) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

1080 

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

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

1082 
"\<lbrakk>x \<in> S; open S\<rbrakk> \<Longrightarrow> at x within S = at x" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

1083 
by (simp only: at_within_interior interior_open) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

1084 

33175  1085 
lemma Lim_within_open: 
1086 
fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space" 

1087 
assumes"a \<in> S" "open S" 

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

1088 
shows "(f > l)(at a within S) \<longleftrightarrow> (f > l)(at a)" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

1089 
using assms by (simp only: at_within_open) 
33175  1090 

43338  1091 
lemma Lim_within_LIMSEQ: 
1092 
fixes a :: real and L :: "'a::metric_space" 

1093 
assumes "\<forall>S. (\<forall>n. S n \<noteq> a \<and> S n \<in> T) \<and> S > a \<longrightarrow> (\<lambda>n. X (S n)) > L" 

1094 
shows "(X > L) (at a within T)" 

1095 
proof (rule ccontr) 

1096 
assume "\<not> (X > L) (at a within T)" 

1097 
hence "\<exists>r>0. \<forall>s>0. \<exists>x\<in>T. x \<noteq> a \<and> \<bar>x  a\<bar> < s \<and> r \<le> dist (X x) L" 

1098 
unfolding tendsto_iff eventually_within dist_norm by (simp add: not_less[symmetric]) 

1099 
then obtain r where r: "r > 0" "\<And>s. s > 0 \<Longrightarrow> \<exists>x\<in>T{a}. \<bar>x  a\<bar> < s \<and> dist (X x) L \<ge> r" by blast 

1100 

1101 
let ?F = "\<lambda>n::nat. SOME x. x \<in> T \<and> x \<noteq> a \<and> \<bar>x  a\<bar> < inverse (real (Suc n)) \<and> dist (X x) L \<ge> r" 

1102 
have "\<And>n. \<exists>x. x \<in> T \<and> x \<noteq> a \<and> \<bar>x  a\<bar> < inverse (real (Suc n)) \<and> dist (X x) L \<ge> r" 

1103 
using r by (simp add: Bex_def) 

1104 
hence F: "\<And>n. ?F n \<in> T \<and> ?F n \<noteq> a \<and> \<bar>?F n  a\<bar> < inverse (real (Suc n)) \<and> dist (X (?F n)) L \<ge> r" 

1105 
by (rule someI_ex) 

1106 
hence F1: "\<And>n. ?F n \<in> T \<and> ?F n \<noteq> a" 

1107 
and F2: "\<And>n. \<bar>?F n  a\<bar> < inverse (real (Suc n))" 

1108 
and F3: "\<And>n. dist (X (?F n)) L \<ge> r" 

1109 
by fast+ 

1110 

1111 
have "?F > a" 

1112 
proof (rule LIMSEQ_I, unfold real_norm_def) 

1113 
fix e::real 

1114 
assume "0 < e" 

1115 
(* choose no such that inverse (real (Suc n)) < e *) 

1116 
then have "\<exists>no. inverse (real (Suc no)) < e" by (rule reals_Archimedean) 

1117 
then obtain m where nodef: "inverse (real (Suc m)) < e" by auto 

1118 
show "\<exists>no. \<forall>n. no \<le> n > \<bar>?F n  a\<bar> < e" 

1119 
proof (intro exI allI impI) 

1120 
fix n 

1121 
assume mlen: "m \<le> n" 

1122 
have "\<bar>?F n  a\<bar> < inverse (real (Suc n))" 

1123 
by (rule F2) 

1124 
also have "inverse (real (Suc n)) \<le> inverse (real (Suc m))" 

1125 
using mlen by auto 

1126 
also from nodef have 

1127 
"inverse (real (Suc m)) < e" . 

1128 
finally show "\<bar>?F n  a\<bar> < e" . 

1129 
qed 

1130 
qed 

1131 
moreover note `\<forall>S. (\<forall>n. S n \<noteq> a \<and> S n \<in> T) \<and> S > a \<longrightarrow> (\<lambda>n. X (S n)) > L` 

1132 
ultimately have "(\<lambda>n. X (?F n)) > L" using F1 by simp 

1133 

1134 
moreover have "\<not> ((\<lambda>n. X (?F n)) > L)" 

1135 
proof  

1136 
{ 

1137 
fix no::nat 

1138 
obtain n where "n = no + 1" by simp 

1139 
then have nolen: "no \<le> n" by simp 

1140 
(* We prove this by showing that for any m there is an n\<ge>m such that X (?F n)  L \<ge> r *) 

1141 
have "dist (X (?F n)) L \<ge> r" 

1142 
by (rule F3) 

1143 
with nolen have "\<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> r" by fast 

1144 
} 

1145 
then have "(\<forall>no. \<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> r)" by simp 

1146 
with r have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> e)" by auto 

1147 
thus ?thesis by (unfold LIMSEQ_def, auto simp add: not_less) 

1148 
qed 

1149 
ultimately show False by simp 

1150 
qed 

1151 

1152 
lemma Lim_right_bound: 

1153 
fixes f :: "real \<Rightarrow> real" 

1154 
assumes mono: "\<And>a b. a \<in> I \<Longrightarrow> b \<in> I \<Longrightarrow> x < a \<Longrightarrow> a \<le> b \<Longrightarrow> f a \<le> f b" 

1155 
assumes bnd: "\<And>a. a \<in> I \<Longrightarrow> x < a \<Longrightarrow> K \<le> f a" 

1156 
shows "(f > Inf (f ` ({x<..} \<inter> I))) (at x within ({x<..} \<inter> I))" 

1157 
proof cases 

1158 
assume "{x<..} \<inter> I = {}" then show ?thesis by (simp add: Lim_within_empty) 

1159 
next 

1160 
assume [simp]: "{x<..} \<inter> I \<noteq> {}" 

1161 
show ?thesis 

1162 
proof (rule Lim_within_LIMSEQ, safe) 

1163 
fix S assume S: "\<forall>n. S n \<noteq> x \<and> S n \<in> {x <..} \<inter> I" "S > x" 

1164 

1165 
show "(\<lambda>n. f (S n)) > Inf (f ` ({x<..} \<inter> I))" 

1166 
proof (rule LIMSEQ_I, rule ccontr) 

1167 
fix r :: real assume "0 < r" 

1168 
with Inf_close[of "f ` ({x<..} \<inter> I)" r] 

1169 
obtain y where y: "x < y" "y \<in> I" "f y < Inf (f ` ({x <..} \<inter> I)) + r" by auto 

1170 
from `x < y` have "0 < y  x" by auto 

1171 
from S(2)[THEN LIMSEQ_D, OF this] 

1172 
obtain N where N: "\<And>n. N \<le> n \<Longrightarrow> \<bar>S n  x\<bar> < y  x" by auto 

1173 

1174 
assume "\<not> (\<exists>N. \<forall>n\<ge>N. norm (f (S n)  Inf (f ` ({x<..} \<inter> I))) < r)" 

1175 
moreover have "\<And>n. Inf (f ` ({x<..} \<inter> I)) \<le> f (S n)" 

1176 
using S bnd by (intro Inf_lower[where z=K]) auto 

1177 
ultimately obtain n where n: "N \<le> n" "r + Inf (f ` ({x<..} \<inter> I)) \<le> f (S n)" 

1178 
by (auto simp: not_less field_simps) 

1179 
with N[OF n(1)] mono[OF _ `y \<in> I`, of "S n"] S(1)[THEN spec, of n] y 

1180 
show False by auto 

1181 
qed 

1182 
qed 

1183 
qed 

1184 

33175  1185 
text{* Another limit point characterization. *} 
1186 

1187 
lemma islimpt_sequential: 

36667  1188 
fixes x :: "'a::metric_space" 
33175  1189 
shows "x islimpt S \<longleftrightarrow> (\<exists>f. (\<forall>n::nat. f n \<in> S {x}) \<and> (f > x) sequentially)" 
1190 
(is "?lhs = ?rhs") 

1191 
proof 

1192 
assume ?lhs 

1193 
then obtain f where f:"\<forall>y. y>0 \<longrightarrow> f y \<in> S \<and> f y \<noteq> x \<and> dist (f y) x < y" 

1194 
unfolding islimpt_approachable using choice[of "\<lambda>e y. e>0 \<longrightarrow> y\<in>S \<and> y\<noteq>x \<and> dist y x < e"] by auto 

1195 
{ fix n::nat 

1196 
have "f (inverse (real n + 1)) \<in> S  {x}" using f by auto 

1197 
} 

1198 
moreover 

1199 
{ fix e::real assume "e>0" 

1200 
hence "\<exists>N::nat. inverse (real (N + 1)) < e" using real_arch_inv[of e] apply (auto simp add: Suc_pred') apply(rule_tac x="n  1" in exI) by auto 

1201 
then obtain N::nat where "inverse (real (N + 1)) < e" by auto 

1202 
hence "\<forall>n\<ge>N. inverse (real n + 1) < e" by (auto, metis Suc_le_mono le_SucE less_imp_inverse_less nat_le_real_less order_less_trans real_of_nat_Suc real_of_nat_Suc_gt_zero) 

1203 
moreover have "\<forall>n\<ge>N. dist (f (inverse (real n + 1))) x < (inverse (real n + 1))" using f `e>0` by auto 

1204 
ultimately have "\<exists>N::nat. \<forall>n\<ge>N. dist (f (inverse (real n + 1))) x < e" apply(rule_tac x=N in exI) apply auto apply(erule_tac x=n in allE)+ by auto 

1205 
} 

1206 
hence " ((\<lambda>n. f (inverse (real n + 1))) > x) sequentially" 

1207 
unfolding Lim_sequentially using f by auto 

1208 
ultimately show ?rhs apply (rule_tac x="(\<lambda>n::nat. f (inverse (real n + 1)))" in exI) by auto 

1209 
next 

1210 
assume ?rhs 

1211 
then obtain f::"nat\<Rightarrow>'a" where f:"(\<forall>n. f n \<in> S  {x})" "(\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (f n) x < e)" unfolding Lim_sequentially by auto 

1212 
{ fix e::real assume "e>0" 

1213 
then obtain N where "dist (f N) x < e" using f(2) by auto 

1214 
moreover have "f N\<in>S" "f N \<noteq> x" using f(1) by auto 

1215 
ultimately have "\<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e" by auto 

1216 
} 

1217 
thus ?lhs unfolding islimpt_approachable by auto 

1218 
qed 

1219 

44125  1220 
lemma Lim_inv: (* TODO: delete *) 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44076
diff
changeset

1221 
fixes f :: "'a \<Rightarrow> real" and A :: "'a filter" 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44076
diff
changeset

1222 
assumes "(f > l) A" and "l \<noteq> 0" 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44076
diff
changeset

1223 
shows "((inverse o f) > inverse l) A" 
36437  1224 
unfolding o_def using assms by (rule tendsto_inverse) 
1225 

33175  1226 
lemma Lim_null: 
1227 
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" 

44125  1228 
shows "(f > l) net \<longleftrightarrow> ((\<lambda>x. f(x)  l) > 0) net" 
33175  1229 
by (simp add: Lim dist_norm) 
1230 

1231 
lemma Lim_null_comparison: 

1232 
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" 

1233 
assumes "eventually (\<lambda>x. norm (f x) \<le> g x) net" "(g > 0) net" 

1234 
shows "(f > 0) net" 
