author  hoelzl 
Mon, 25 Jan 2010 16:56:24 +0100  
changeset 34964  4e8be3c04d37 
parent 34291  4e896680897e 
child 34999  5312d2ffee3b 
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 

4 
*) 

5 

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

7 

8 
theory Topology_Euclidean_Space 

9 
imports SEQ Euclidean_Space Product_Vector 

10 
begin 

11 

12 
subsection{* General notion of a topology *} 

13 

14 
definition "istopology L \<longleftrightarrow> {} \<in> L \<and> (\<forall>S \<in>L. \<forall>T \<in>L. S \<inter> T \<in> L) \<and> (\<forall>K. K \<subseteq>L \<longrightarrow> \<Union> K \<in> L)" 

15 
typedef (open) 'a topology = "{L::('a set) set. istopology L}" 

16 
morphisms "openin" "topology" 

17 
unfolding istopology_def by blast 

18 

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

20 
using openin[of U] by blast 

21 

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

23 
using topology_inverse[unfolded mem_def Collect_def] . 

24 

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

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

27 

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

29 
proof 

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

31 
moreover 

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

33 
hence "openin T1 = openin T2" by (metis mem_def set_ext) 

34 
hence "topology (openin T1) = topology (openin T2)" by simp 

35 
hence "T1 = T2" unfolding openin_inverse .} 

36 
ultimately show ?thesis by blast 

37 
qed 

38 

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

40 

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

42 

43 
subsection{* Main properties of open sets *} 

44 

45 
lemma openin_clauses: 

46 
fixes U :: "'a topology" 

47 
shows "openin U {}" 

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

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

50 
using openin[of U] unfolding istopology_def Collect_def mem_def 

51 
by (metis mem_def subset_eq)+ 

52 

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

54 
unfolding topspace_def by blast 

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

56 

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

58 
by (simp add: openin_clauses) 

59 

60 
lemma openin_Union[intro]: "(\<forall>S \<in>K. openin U S) \<Longrightarrow> openin U (\<Union> K)" by (simp add: openin_clauses) 

61 

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

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

64 

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

66 

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

68 
proof 

69 
{assume ?lhs then have ?rhs by auto } 

70 
moreover 

71 
{assume H: ?rhs 

72 
then obtain t where t: "\<forall>x\<in>S. openin U (t x) \<and> x \<in> t x \<and> t x \<subseteq> S" 

73 
unfolding Ball_def ex_simps(6)[symmetric] choice_iff by blast 

74 
from t have th0: "\<forall>x\<in> t`S. openin U x" by auto 

75 
have "\<Union> t`S = S" using t by auto 

76 
with openin_Union[OF th0] have "openin U S" by simp } 

77 
ultimately show ?thesis by blast 

78 
qed 

79 

80 
subsection{* Closed sets *} 

81 

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

83 

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

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

86 
lemma closedin_topspace[intro,simp]: 

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

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

89 
by (auto simp add: Diff_Un closedin_def) 

90 

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

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

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

94 

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

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

97 

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

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

100 
apply (auto simp add: closedin_def Diff_Diff_Int inf_absorb2) 

101 
apply (metis openin_subset subset_eq) 

102 
done 

103 

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

105 
by (simp add: openin_closedin_eq) 

106 

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

108 
proof 

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

110 
by (auto simp add: topspace_def openin_subset) 

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

112 
qed 

113 

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

115 
proof 

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

117 
by (auto simp add: topspace_def ) 

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

119 
qed 

120 

121 
subsection{* Subspace topology. *} 

122 

123 
definition "subtopology U V = topology {S \<inter> V S. openin U S}" 

124 

125 
lemma istopology_subtopology: "istopology {S \<inter> V S. openin U S}" (is "istopology ?L") 

126 
proof 

127 
have "{} \<in> ?L" by blast 

128 
{fix A B assume A: "A \<in> ?L" and B: "B \<in> ?L" 

129 
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 

130 
have "A\<inter>B = (Sa \<inter> Sb) \<inter> V" "openin U (Sa \<inter> Sb)" using Sa Sb by blast+ 

131 
then have "A \<inter> B \<in> ?L" by blast} 

132 
moreover 

133 
{fix K assume K: "K \<subseteq> ?L" 

134 
have th0: "?L = (\<lambda>S. S \<inter> V) ` openin U " 

135 
apply (rule set_ext) 

136 
apply (simp add: Ball_def image_iff) 

137 
by (metis mem_def) 

138 
from K[unfolded th0 subset_image_iff] 

139 
obtain Sk where Sk: "Sk \<subseteq> openin U" "K = (\<lambda>S. S \<inter> V) ` Sk" by blast 

140 
have "\<Union>K = (\<Union>Sk) \<inter> V" using Sk by auto 

141 
moreover have "openin U (\<Union> Sk)" using Sk by (auto simp add: subset_eq mem_def) 

142 
ultimately have "\<Union>K \<in> ?L" by blast} 

143 
ultimately show ?thesis unfolding istopology_def by blast 

144 
qed 

145 

146 
lemma openin_subtopology: 

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

148 
unfolding subtopology_def topology_inverse'[OF istopology_subtopology] 

149 
by (auto simp add: Collect_def) 

150 

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

152 
by (auto simp add: topspace_def openin_subtopology) 

153 

154 
lemma closedin_subtopology: 

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

156 
unfolding closedin_def topspace_subtopology 

157 
apply (simp add: openin_subtopology) 

158 
apply (rule iffI) 

159 
apply clarify 

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

161 
by auto 

162 

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

164 
unfolding openin_subtopology 

165 
apply (rule iffI, clarify) 

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

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

168 
by auto 

169 

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

171 
shows "subtopology U V = U" 

172 
proof 

173 
{fix S 

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

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

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

177 
moreover 

178 
{assume S: "openin U S" 

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

180 
using openin_subset[OF S] UV by auto} 

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

182 
then show ?thesis unfolding topology_eq openin_subtopology by blast 

183 
qed 

184 

185 

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

187 
by (simp add: subtopology_superset) 

188 

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

190 
by (simp add: subtopology_superset) 

191 

192 
subsection{* The universal Euclidean versions are what we use most of the time *} 

193 

194 
definition 

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

196 
"euclidean = topology open" 

197 

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

199 
unfolding euclidean_def 

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

201 
apply (rule topology_inverse[symmetric]) 

202 
apply (auto simp add: istopology_def) 

203 
by (auto simp add: mem_def subset_eq) 

204 

205 
lemma topspace_euclidean: "topspace euclidean = UNIV" 

206 
apply (simp add: topspace_def) 

207 
apply (rule set_ext) 

208 
by (auto simp add: open_openin[symmetric]) 

209 

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

211 
by (simp add: topspace_euclidean topspace_subtopology) 

212 

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

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

215 

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

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

218 

219 
subsection{* Open and closed balls. *} 

220 

221 
definition 

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

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

224 

225 
definition 

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

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

228 

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

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

231 

232 
lemma mem_ball_0 [simp]: 

233 
fixes x :: "'a::real_normed_vector" 

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

235 
by (simp add: dist_norm) 

236 

237 
lemma mem_cball_0 [simp]: 

238 
fixes x :: "'a::real_normed_vector" 

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

240 
by (simp add: dist_norm) 

241 

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

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

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

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

246 
lemma ball_max_Un: "ball a (max r s) = ball a r \<union> ball a s" 

247 
by (simp add: expand_set_eq) arith 

248 

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

250 
by (simp add: expand_set_eq) 

251 

252 
subsection{* Topological properties of open balls *} 

253 

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

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

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

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

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

259 

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

261 
unfolding open_dist ball_def Collect_def Ball_def mem_def 

262 
unfolding dist_commute 

263 
apply clarify 

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

265 
using dist_triangle_alt[where z=x] 

266 
apply (clarsimp simp add: diff_less_iff) 

267 
apply atomize 

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

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

270 
by arith 

271 

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

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

274 
unfolding open_dist subset_eq mem_ball Ball_def dist_commute .. 

275 

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

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

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

278 
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

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

280 

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

283 

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

285 
unfolding mem_ball expand_set_eq 

286 
apply (simp add: not_less) 

287 
by (metis zero_le_dist order_trans dist_self) 

288 

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

290 

291 
subsection{* Basic "localization" results are handy for connectedness. *} 

292 

293 
lemma openin_open: "openin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. open T \<and> (S = U \<inter> T))" 

294 
by (auto simp add: openin_subtopology open_openin[symmetric]) 

295 

296 
lemma openin_open_Int[intro]: "open S \<Longrightarrow> openin (subtopology euclidean U) (U \<inter> S)" 

297 
by (auto simp add: openin_open) 

298 

299 
lemma open_openin_trans[trans]: 

300 
"open S \<Longrightarrow> open T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> openin (subtopology euclidean S) T" 

301 
by (metis Int_absorb1 openin_open_Int) 

302 

303 
lemma open_subset: "S \<subseteq> T \<Longrightarrow> open S \<Longrightarrow> openin (subtopology euclidean T) S" 

304 
by (auto simp add: openin_open) 

305 

306 
lemma closedin_closed: "closedin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. closed T \<and> S = U \<inter> T)" 

307 
by (simp add: closedin_subtopology closed_closedin Int_ac) 

308 

309 
lemma closedin_closed_Int: "closed S ==> closedin (subtopology euclidean U) (U \<inter> S)" 

310 
by (metis closedin_closed) 

311 

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

313 
apply (subgoal_tac "S \<inter> T = T" ) 

314 
apply auto 

315 
apply (frule closedin_closed_Int[of T S]) 

316 
by simp 

317 

318 
lemma closed_subset: "S \<subseteq> T \<Longrightarrow> closed S \<Longrightarrow> closedin (subtopology euclidean T) S" 

319 
by (auto simp add: closedin_closed) 

320 

321 
lemma openin_euclidean_subtopology_iff: 

322 
fixes S U :: "'a::metric_space set" 

323 
shows "openin (subtopology euclidean U) S 

324 
\<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") 

325 
proof 

326 
{assume ?lhs hence ?rhs unfolding openin_subtopology open_openin[symmetric] 

327 
by (simp add: open_dist) blast} 

328 
moreover 

329 
{assume SU: "S \<subseteq> U" and H: "\<And>x. x \<in> S \<Longrightarrow> \<exists>e>0. \<forall>x'\<in>U. dist x' x < e \<longrightarrow> x' \<in> S" 

330 
from H obtain d where d: "\<And>x . x\<in> S \<Longrightarrow> d x > 0 \<and> (\<forall>x' \<in> U. dist x' x < d x \<longrightarrow> x' \<in> S)" 

331 
by metis 

332 
let ?T = "\<Union>{B. \<exists>x\<in>S. B = ball x (d x)}" 

333 
have oT: "open ?T" by auto 

334 
{ fix x assume "x\<in>S" 

335 
hence "x \<in> \<Union>{B. \<exists>x\<in>S. B = ball x (d x)}" 

336 
apply simp apply(rule_tac x="ball x(d x)" in exI) apply auto 

337 
by (rule d [THEN conjunct1]) 

338 
hence "x\<in> ?T \<inter> U" using SU and `x\<in>S` by auto } 

339 
moreover 

340 
{ fix y assume "y\<in>?T" 

341 
then obtain B where "y\<in>B" "B\<in>{B. \<exists>x\<in>S. B = ball x (d x)}" by auto 

342 
then obtain x where "x\<in>S" and x:"y \<in> ball x (d x)" by auto 

343 
assume "y\<in>U" 

344 
hence "y\<in>S" using d[OF `x\<in>S`] and x by(auto simp add: dist_commute) } 

345 
ultimately have "S = ?T \<inter> U" by blast 

346 
with oT have ?lhs unfolding openin_subtopology open_openin[symmetric] by blast} 

347 
ultimately show ?thesis by blast 

348 
qed 

349 

350 
text{* These "transitivity" results are handy too. *} 

351 

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

353 
\<Longrightarrow> openin (subtopology euclidean U) S" 

354 
unfolding open_openin openin_open by blast 

355 

356 
lemma openin_open_trans: "openin (subtopology euclidean T) S \<Longrightarrow> open T \<Longrightarrow> open S" 

357 
by (auto simp add: openin_open intro: openin_trans) 

358 

359 
lemma closedin_trans[trans]: 

360 
"closedin (subtopology euclidean T) S \<Longrightarrow> 

361 
closedin (subtopology euclidean U) T 

362 
==> closedin (subtopology euclidean U) S" 

363 
by (auto simp add: closedin_closed closed_closedin closed_Inter Int_assoc) 

364 

365 
lemma closedin_closed_trans: "closedin (subtopology euclidean T) S \<Longrightarrow> closed T \<Longrightarrow> closed S" 

366 
by (auto simp add: closedin_closed intro: closedin_trans) 

367 

368 
subsection{* Connectedness *} 

369 

370 
definition "connected S \<longleftrightarrow> 

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

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

373 

374 
lemma connected_local: 

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

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

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

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

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

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

381 
~(e2 = {}))" 

382 
unfolding connected_def openin_open by (safe, blast+) 

383 

34105  384 
lemma exists_diff: 
385 
fixes P :: "'a set \<Rightarrow> bool" 

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

33175  387 
proof 
388 
{assume "?lhs" hence ?rhs by blast } 

389 
moreover 

390 
{fix S assume H: "P S" 

34105  391 
have "S =  ( S)" by auto 
392 
with H have "P ( ( S))" by metis } 

33175  393 
ultimately show ?thesis by metis 
394 
qed 

395 

396 
lemma connected_clopen: "connected S \<longleftrightarrow> 

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

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

399 
proof 

34105  400 
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  401 
unfolding connected_def openin_open closedin_closed 
402 
apply (subst exists_diff) by blast 

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

33175  405 

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

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

408 
unfolding connected_def openin_open closedin_closed by auto 

409 
{fix e2 

410 
{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)" 

411 
by auto} 

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

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

414 
then show ?thesis unfolding th0 th1 by simp 

415 
qed 

416 

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

418 
by (simp add: connected_def) 

419 

420 
subsection{* Hausdorff and other separation properties *} 

421 

422 
class t0_space = 

423 
assumes t0_space: "x \<noteq> y \<Longrightarrow> \<exists>U. open U \<and> \<not> (x \<in> U \<longleftrightarrow> y \<in> U)" 

424 

425 
class t1_space = 

426 
assumes t1_space: "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<notin> U \<and> x \<notin> V \<and> y \<in> V" 

427 
begin 

428 

429 
subclass t0_space 

430 
proof 

431 
qed (fast dest: t1_space) 

432 

433 
end 

434 

435 
text {* T2 spaces are also known as Hausdorff spaces. *} 

436 

437 
class t2_space = 

438 
assumes hausdorff: "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}" 

439 
begin 

440 

441 
subclass t1_space 

442 
proof 

443 
qed (fast dest: hausdorff) 

444 

445 
end 

446 

447 
instance metric_space \<subseteq> t2_space 

448 
proof 

449 
fix x y :: "'a::metric_space" 

450 
assume xy: "x \<noteq> y" 

451 
let ?U = "ball x (dist x y / 2)" 

452 
let ?V = "ball y (dist x y / 2)" 

453 
have th0: "\<And>d x y z. (d x z :: real) <= d x y + d y z \<Longrightarrow> d y z = d z y 

454 
==> ~(d x y * 2 < d x z \<and> d z y * 2 < d x z)" by arith 

455 
have "open ?U \<and> open ?V \<and> x \<in> ?U \<and> y \<in> ?V \<and> ?U \<inter> ?V = {}" 

456 
using dist_pos_lt[OF xy] th0[of dist,OF dist_triangle dist_commute] 

457 
by (auto simp add: expand_set_eq) 

458 
then show "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}" 

459 
by blast 

460 
qed 

461 

462 
lemma separation_t2: 

463 
fixes x y :: "'a::t2_space" 

464 
shows "x \<noteq> y \<longleftrightarrow> (\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {})" 

465 
using hausdorff[of x y] by blast 

466 

467 
lemma separation_t1: 

468 
fixes x y :: "'a::t1_space" 

469 
shows "x \<noteq> y \<longleftrightarrow> (\<exists>U V. open U \<and> open V \<and> x \<in>U \<and> y\<notin> U \<and> x\<notin>V \<and> y\<in>V)" 

470 
using t1_space[of x y] by blast 

471 

472 
lemma separation_t0: 

473 
fixes x y :: "'a::t0_space" 

474 
shows "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> ~(x\<in>U \<longleftrightarrow> y\<in>U))" 

475 
using t0_space[of x y] by blast 

476 

477 
subsection{* Limit points *} 

478 

479 
definition 

480 
islimpt:: "'a::topological_space \<Rightarrow> 'a set \<Rightarrow> bool" 

481 
(infixr "islimpt" 60) where 

482 
"x islimpt S \<longleftrightarrow> (\<forall>T. x\<in>T \<longrightarrow> open T \<longrightarrow> (\<exists>y\<in>S. y\<in>T \<and> y\<noteq>x))" 

483 

484 
lemma islimptI: 

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

486 
shows "x islimpt S" 

487 
using assms unfolding islimpt_def by auto 

488 

489 
lemma islimptE: 

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

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

492 
using assms unfolding islimpt_def by auto 

493 

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

495 

496 
lemma islimpt_approachable: 

497 
fixes x :: "'a::metric_space" 

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

499 
unfolding islimpt_def 

500 
apply auto 

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

502 
apply auto 

503 
apply(rule_tac x=y in bexI) 

504 
apply (auto simp add: dist_commute) 

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

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

507 
done 

508 

509 
lemma islimpt_approachable_le: 

510 
fixes x :: "'a::metric_space" 

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

512 
unfolding islimpt_approachable 

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

33324  514 
by metis 
33175  515 

516 
class perfect_space = 

517 
(* FIXME: perfect_space should inherit from topological_space *) 

518 
assumes islimpt_UNIV [simp, intro]: "(x::'a::metric_space) islimpt UNIV" 

519 

520 
lemma perfect_choose_dist: 

521 
fixes x :: "'a::perfect_space" 

522 
shows "0 < r \<Longrightarrow> \<exists>a. a \<noteq> x \<and> dist a x < r" 

523 
using islimpt_UNIV [of x] 

524 
by (simp add: islimpt_approachable) 

525 

526 
instance real :: perfect_space 

527 
apply default 

528 
apply (rule islimpt_approachable [THEN iffD2]) 

529 
apply (clarify, rule_tac x="x + e/2" in bexI) 

530 
apply (auto simp add: dist_norm) 

531 
done 

532 

34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34289
diff
changeset

533 
instance cart :: (perfect_space, finite) perfect_space 
33175  534 
proof 
535 
fix x :: "'a ^ 'b" 

536 
{ 

537 
fix e :: real assume "0 < e" 

538 
def a \<equiv> "x $ undefined" 

539 
have "a islimpt UNIV" by (rule islimpt_UNIV) 

540 
with `0 < e` obtain b where "b \<noteq> a" and "dist b a < e" 

541 
unfolding islimpt_approachable by auto 

542 
def y \<equiv> "Cart_lambda ((Cart_nth x)(undefined := b))" 

543 
from `b \<noteq> a` have "y \<noteq> x" 

544 
unfolding a_def y_def by (simp add: Cart_eq) 

545 
from `dist b a < e` have "dist y x < e" 

546 
unfolding dist_vector_def a_def y_def 

547 
apply simp 

548 
apply (rule le_less_trans [OF setL2_le_setsum [OF zero_le_dist]]) 

549 
apply (subst setsum_diff1' [where a=undefined], simp, simp, simp) 

550 
done 

551 
from `y \<noteq> x` and `dist y x < e` 

552 
have "\<exists>y\<in>UNIV. y \<noteq> x \<and> dist y x < e" by auto 

553 
} 

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

555 
qed 

556 

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

558 
unfolding closed_def 

559 
apply (subst open_subopen) 

34105  560 
apply (simp add: islimpt_def subset_eq) 
561 
by (metis ComplE ComplI insertCI insert_absorb mem_def) 

33175  562 

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

564 
unfolding islimpt_def by auto 

565 

34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34289
diff
changeset

566 
lemma closed_positive_orthant: "closed {x::real^'n. \<forall>i. 0 \<le>x$i}" 
33175  567 
proof 
568 
let ?U = "UNIV :: 'n set" 

569 
let ?O = "{x::real^'n. \<forall>i. x$i\<ge>0}" 

570 
{fix x:: "real^'n" and i::'n assume H: "\<forall>e>0. \<exists>x'\<in>?O. x' \<noteq> x \<and> dist x' x < e" 

571 
and xi: "x$i < 0" 

572 
from xi have th0: "x$i > 0" by arith 

573 
from H[rule_format, OF th0] obtain x' where x': "x' \<in>?O" "x' \<noteq> x" "dist x' x < x $ i" by blast 

574 
have th:" \<And>b a (x::real). abs x <= b \<Longrightarrow> b <= a ==> ~(a + x < 0)" by arith 

575 
have th': "\<And>x (y::real). x < 0 \<Longrightarrow> 0 <= y ==> abs x <= abs (y  x)" by arith 

576 
have th1: "\<bar>x$i\<bar> \<le> \<bar>(x'  x)$i\<bar>" using x'(1) xi 

577 
apply (simp only: vector_component) 

578 
by (rule th') auto 

579 
have th2: "\<bar>dist x x'\<bar> \<ge> \<bar>(x'  x)$i\<bar>" using component_le_norm[of "x'x" i] 

580 
apply (simp add: dist_norm) by norm 

581 
from th[OF th1 th2] x'(3) have False by (simp add: dist_commute) } 

582 
then show ?thesis unfolding closed_limpt islimpt_approachable 

583 
unfolding not_le[symmetric] by blast 

584 
qed 

585 

586 
lemma finite_set_avoid: 

587 
fixes a :: "'a::metric_space" 

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

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

590 
case 1 thus ?case apply auto by ferrack 

591 
next 

592 
case (2 x F) 

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

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

595 
moreover 

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

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

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

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

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

601 
ultimately show ?case by blast 

602 
qed 

603 

604 
lemma islimpt_finite: 

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

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

607 
unfolding islimpt_approachable 

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

609 

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

611 
apply (rule iffI) 

612 
defer 

613 
apply (metis Un_upper1 Un_upper2 islimpt_subset) 

614 
unfolding islimpt_def 

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

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

617 
apply (auto simp add: open_Int) 

618 
done 

619 

620 
lemma discrete_imp_closed: 

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

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

623 
shows "closed S" 

624 
proof 

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

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

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

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

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

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

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

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

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

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

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

636 
qed 

637 

638 
subsection{* Interior of a Set *} 

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

640 

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

642 
apply (simp add: expand_set_eq interior_def) 

643 
apply (subst (2) open_subopen) by (safe, blast+) 

644 

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

646 

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

648 

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

650 
apply (simp add: interior_def) 

651 
apply (subst open_subopen) by blast 

652 

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

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

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

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

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

658 
by (metis equalityI interior_maximal interior_subset open_interior) 

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

660 
apply (simp add: interior_def) 

661 
by (metis open_contains_ball centre_in_ball open_ball subset_trans) 

662 

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

664 
by (metis interior_maximal interior_subset subset_trans) 

665 

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

667 
apply (rule equalityI, simp) 

668 
apply (metis Int_lower1 Int_lower2 subset_interior) 

669 
by (metis Int_mono interior_subset open_Int open_interior open_subset_interior) 

670 

671 
lemma interior_limit_point [intro]: 

672 
fixes x :: "'a::perfect_space" 

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

674 
proof 

675 
from x obtain e where e: "e>0" "\<forall>x'. dist x x' < e \<longrightarrow> x' \<in> S" 

676 
unfolding mem_interior subset_eq Ball_def mem_ball by blast 

677 
{ 

678 
fix d::real assume d: "d>0" 

679 
let ?m = "min d e" 

680 
have mde2: "0 < ?m" using e(1) d(1) by simp 

681 
from perfect_choose_dist [OF mde2, of x] 

682 
obtain y where "y \<noteq> x" and "dist y x < ?m" by blast 

683 
then have "dist y x < e" "dist y x < d" by simp_all 

684 
from `dist y x < e` e(2) have "y \<in> S" by (simp add: dist_commute) 

685 
have "\<exists>x'\<in>S. x'\<noteq> x \<and> dist x' x < d" 

686 
using `y \<in> S` `y \<noteq> x` `dist y x < d` by fast 

687 
} 

688 
then show ?thesis unfolding islimpt_approachable by blast 

689 
qed 

690 

691 
lemma interior_closed_Un_empty_interior: 

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

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

694 
proof 

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

696 
by (rule subset_interior, blast) 

697 
next 

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

699 
proof 

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

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

702 
unfolding interior_def by fast 

703 
show "x \<in> interior S" 

704 
proof (rule ccontr) 

705 
assume "x \<notin> interior S" 

706 
with `x \<in> R` `open R` obtain y where "y \<in> R  S" 

707 
unfolding interior_def expand_set_eq by fast 

708 
from `open R` `closed S` have "open (R  S)" by (rule open_Diff) 

709 
from `R \<subseteq> S \<union> T` have "R  S \<subseteq> T" by fast 

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

711 
show "False" unfolding interior_def by fast 

712 
qed 

713 
qed 

714 
qed 

715 

716 

717 
subsection{* Closure of a Set *} 

718 

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

720 

34105  721 
lemma closure_interior: "closure S =  interior ( S)" 
33175  722 
proof 
723 
{ fix x 

34105  724 
have "x\<in> interior ( S) \<longleftrightarrow> x \<in> closure S" (is "?lhs = ?rhs") 
33175  725 
proof 
34105  726 
let ?exT = "\<lambda> y. (\<exists>T. open T \<and> y \<in> T \<and> T \<subseteq>  S)" 
33175  727 
assume "?lhs" 
728 
hence *:"\<not> ?exT x" 

729 
unfolding interior_def 

730 
by simp 

731 
{ assume "\<not> ?rhs" 

732 
hence False using * 

733 
unfolding closure_def islimpt_def 

734 
by blast 

735 
} 

736 
thus "?rhs" 

737 
by blast 

738 
next 

739 
assume "?rhs" thus "?lhs" 

740 
unfolding closure_def interior_def islimpt_def 

741 
by blast 

742 
qed 

743 
} 

744 
thus ?thesis 

745 
by blast 

746 
qed 

747 

34105  748 
lemma interior_closure: "interior S =  (closure ( S))" 
33175  749 
proof 
750 
{ fix x 

34105  751 
have "x \<in> interior S \<longleftrightarrow> x \<in>  (closure ( S))" 
33175  752 
unfolding interior_def closure_def islimpt_def 
33324  753 
by auto 
33175  754 
} 
755 
thus ?thesis 

756 
by blast 

757 
qed 

758 

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

760 
proof 

34105  761 
have "closed ( interior (S))" by blast 
33175  762 
thus ?thesis using closure_interior[of S] by simp 
763 
qed 

764 

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

766 
proof 

767 
have "S \<subseteq> closure S" 

768 
unfolding closure_def 

769 
by blast 

770 
moreover 

771 
have "closed (closure S)" 

772 
using closed_closure[of S] 

773 
by assumption 

774 
moreover 

775 
{ fix t 

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

777 
{ fix x 

778 
assume "x islimpt S" 

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

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

781 
by blast 

782 
} 

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

784 
unfolding closure_def 

785 
using closed_limpt[of t] 

786 
by auto 

787 
} 

788 
ultimately show ?thesis 

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

790 
unfolding mem_def 

791 
by simp 

792 
qed 

793 

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

795 
unfolding closure_hull 

796 
using hull_eq[of closed, unfolded mem_def, OF closed_Inter, of S] 

797 
by (metis mem_def subset_eq) 

798 

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

800 
using closure_eq[of S] 

801 
by simp 

802 

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

804 
unfolding closure_hull 

805 
using hull_hull[of closed S] 

806 
by assumption 

807 

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

809 
unfolding closure_hull 

810 
using hull_subset[of S closed] 

811 
by assumption 

812 

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

814 
unfolding closure_hull 

815 
using hull_mono[of S T closed] 

816 
by assumption 

817 

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

819 
using hull_minimal[of S T closed] 

820 
unfolding closure_hull mem_def 

821 
by simp 

822 

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

824 
using hull_unique[of S T closed] 

825 
unfolding closure_hull mem_def 

826 
by simp 

827 

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

829 
using closed_empty closure_closed[of "{}"] 

830 
by simp 

831 

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

833 
using closure_closed[of UNIV] 

834 
by simp 

835 

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

837 
using closure_empty closure_subset[of S] 

838 
by blast 

839 

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

841 
using closure_eq[of S] closure_subset[of S] 

842 
by simp 

843 

844 
lemma open_inter_closure_eq_empty: 

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

34105  846 
using open_subset_interior[of S " T"] 
847 
using interior_subset[of " T"] 

33175  848 
unfolding closure_interior 
849 
by auto 

850 

851 
lemma open_inter_closure_subset: 

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

853 
proof 

854 
fix x 

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

856 
{ assume *:"x islimpt T" 

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

858 
proof (rule islimptI) 

859 
fix A 

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

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

862 
by (simp_all add: open_Int) 

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

864 
by (rule islimptE) 

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

866 
by simp_all 

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

868 
qed 

869 
} 

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

871 
unfolding closure_def 

872 
by blast 

873 
qed 

874 

34105  875 
lemma closure_complement: "closure( S) =  interior(S)" 
33175  876 
proof 
34105  877 
have "S =  ( S)" 
33175  878 
by auto 
879 
thus ?thesis 

880 
unfolding closure_interior 

881 
by auto 

882 
qed 

883 

34105  884 
lemma interior_complement: "interior( S) =  closure(S)" 
33175  885 
unfolding closure_interior 
886 
by blast 

887 

888 
subsection{* Frontier (aka boundary) *} 

889 

890 
definition "frontier S = closure S  interior S" 

891 

892 
lemma frontier_closed: "closed(frontier S)" 

893 
by (simp add: frontier_def closed_Diff) 

894 

34105  895 
lemma frontier_closures: "frontier S = (closure S) \<inter> (closure( S))" 
33175  896 
by (auto simp add: frontier_def interior_closure) 
897 

898 
lemma frontier_straddle: 

899 
fixes a :: "'a::metric_space" 

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

901 
proof 

902 
assume "?lhs" 

903 
{ fix e::real 

904 
assume "e > 0" 

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

906 
{ assume "a\<in>S" 

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

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

909 
unfolding frontier_closures closure_def islimpt_def using `e>0` 

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

911 
ultimately have ?rhse by auto 

912 
} 

913 
moreover 

914 
{ assume "a\<notin>S" 

915 
hence ?rhse using `?lhs` 

916 
unfolding frontier_closures closure_def islimpt_def 

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

33324  918 
by simp (metis centre_in_ball mem_ball open_ball) 
33175  919 
} 
920 
ultimately have ?rhse by auto 

921 
} 

922 
thus ?rhs by auto 

923 
next 

924 
assume ?rhs 

925 
moreover 

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

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

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

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

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

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

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

933 
} 

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

935 
moreover 

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

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

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

34105  939 
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  940 
} 
34105  941 
hence "a islimpt ( S) \<or> a\<notin>S" unfolding islimpt_def by auto 
942 
ultimately show ?lhs unfolding frontier_closures using closure_def[of " S"] by auto 

33175  943 
qed 
944 

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

946 
by (metis frontier_def closure_closed Diff_subset) 

947 

34964  948 
lemma frontier_empty[simp]: "frontier {} = {}" 
33175  949 
by (simp add: frontier_def closure_empty) 
950 

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

952 
proof 

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

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

955 
hence "closed S" using closure_subset_eq by auto 

956 
} 

957 
thus ?thesis using frontier_subset_closed[of S] by auto 

958 
qed 

959 

34105  960 
lemma frontier_complement: "frontier( S) = frontier S" 
33175  961 
by (auto simp add: frontier_def closure_complement interior_complement) 
962 

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

34105  964 
using frontier_complement frontier_subset_eq[of " S"] 
965 
unfolding open_closed by auto 

33175  966 

967 
subsection{* Common nets and The "within" modifier for nets. *} 

968 

969 
definition 

970 
at_infinity :: "'a::real_normed_vector net" where 

971 
"at_infinity = Abs_net (range (\<lambda>r. {x. r \<le> norm x}))" 

972 

973 
definition 

974 
indirection :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> 'a net" (infixr "indirection" 70) where 

975 
"a indirection v = (at a) within {b. \<exists>c\<ge>0. b  a = scaleR c v}" 

976 

977 
text{* Prove That They are all nets. *} 

978 

979 
lemma Rep_net_at_infinity: 

980 
"Rep_net at_infinity = range (\<lambda>r. {x. r \<le> norm x})" 

981 
unfolding at_infinity_def 

982 
apply (rule Abs_net_inverse') 

983 
apply (rule image_nonempty, simp) 

984 
apply (clarsimp, rename_tac r s) 

985 
apply (rule_tac x="max r s" in exI, auto) 

986 
done 

987 

988 
lemma within_UNIV: "net within UNIV = net" 

989 
by (simp add: Rep_net_inject [symmetric] Rep_net_within) 

990 

991 
subsection{* Identify Trivial limits, where we can't approach arbitrarily closely. *} 

992 

993 
definition 

994 
trivial_limit :: "'a net \<Rightarrow> bool" where 

995 
"trivial_limit net \<longleftrightarrow> {} \<in> Rep_net net" 

996 

997 
lemma trivial_limit_within: 

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

999 
proof 

1000 
assume "trivial_limit (at a within S)" 

1001 
thus "\<not> a islimpt S" 

1002 
unfolding trivial_limit_def 

1003 
unfolding Rep_net_within Rep_net_at 

1004 
unfolding islimpt_def 

1005 
apply (clarsimp simp add: expand_set_eq) 

1006 
apply (rename_tac T, rule_tac x=T in exI) 

1007 
apply (clarsimp, drule_tac x=y in spec, simp) 

1008 
done 

1009 
next 

1010 
assume "\<not> a islimpt S" 

1011 
thus "trivial_limit (at a within S)" 

1012 
unfolding trivial_limit_def 

1013 
unfolding Rep_net_within Rep_net_at 

1014 
unfolding islimpt_def 

1015 
apply (clarsimp simp add: image_image) 

1016 
apply (rule_tac x=T in image_eqI) 

1017 
apply (auto simp add: expand_set_eq) 

1018 
done 

1019 
qed 

1020 

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

1022 
using trivial_limit_within [of a UNIV] 

1023 
by (simp add: within_UNIV) 

1024 

1025 
lemma trivial_limit_at: 

1026 
fixes a :: "'a::perfect_space" 

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

1028 
by (simp add: trivial_limit_at_iff) 

1029 

1030 
lemma trivial_limit_at_infinity: 

1031 
"\<not> trivial_limit (at_infinity :: ('a::{real_normed_vector,zero_neq_one}) net)" 

1032 
(* FIXME: find a more appropriate type class *) 

1033 
unfolding trivial_limit_def Rep_net_at_infinity 

1034 
apply (clarsimp simp add: expand_set_eq) 

1035 
apply (drule_tac x="scaleR r (sgn 1)" in spec) 

1036 
apply (simp add: norm_sgn) 

1037 
done 

1038 

34964  1039 
lemma trivial_limit_sequentially[intro]: "\<not> trivial_limit sequentially" 
33175  1040 
by (auto simp add: trivial_limit_def Rep_net_sequentially) 
1041 

1042 
subsection{* Some property holds "sufficiently close" to the limit point. *} 

1043 

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

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

1046 
unfolding eventually_at dist_nz by auto 

1047 

1048 
lemma eventually_at_infinity: 

1049 
"eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. norm x >= b \<longrightarrow> P x)" 

1050 
unfolding eventually_def Rep_net_at_infinity by auto 

1051 

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

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

1054 
unfolding eventually_within eventually_at dist_nz by auto 

1055 

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

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

1058 
unfolding eventually_within 

33324  1059 
by auto (metis Rats_dense_in_nn_real order_le_less_trans order_refl) 
33175  1060 

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

1062 
unfolding eventually_def trivial_limit_def 

1063 
using Rep_net_nonempty [of net] by auto 

1064 

1065 
lemma always_eventually: "(\<forall>x. P x) ==> eventually P net" 

1066 
unfolding eventually_def trivial_limit_def 

1067 
using Rep_net_nonempty [of net] by auto 

1068 

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

1070 
unfolding trivial_limit_def eventually_def by auto 

1071 

1072 
lemma eventually_False: "eventually (\<lambda>x. False) net \<longleftrightarrow> trivial_limit net" 

1073 
unfolding trivial_limit_def eventually_def by auto 

1074 

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

1076 
apply (safe elim!: trivial_limit_eventually) 

1077 
apply (simp add: eventually_False [symmetric]) 

1078 
done 

1079 

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

1081 

1082 
lemma eventually_conjI: 

1083 
"\<lbrakk>eventually (\<lambda>x. P x) net; eventually (\<lambda>x. Q x) net\<rbrakk> 

1084 
\<Longrightarrow> eventually (\<lambda>x. P x \<and> Q x) net" 

1085 
by (rule eventually_conj) 

1086 

1087 
lemma eventually_rev_mono: 

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

1089 
using eventually_mono [of P Q] by fast 

1090 

1091 
lemma eventually_and: " eventually (\<lambda>x. P x \<and> Q x) net \<longleftrightarrow> eventually P net \<and> eventually Q net" 

1092 
by (auto intro!: eventually_conjI elim: eventually_rev_mono) 

1093 

1094 
lemma eventually_false: "eventually (\<lambda>x. False) net \<longleftrightarrow> trivial_limit net" 

1095 
by (auto simp add: eventually_False) 

1096 

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

1098 
by (simp add: eventually_False) 

1099 

1100 
subsection{* Limits, defined as vacuously true when the limit is trivial. *} 

1101 

1102 
text{* Notation Lim to avoid collition with lim defined in analysis *} 

1103 
definition 

1104 
Lim :: "'a net \<Rightarrow> ('a \<Rightarrow> 'b::t2_space) \<Rightarrow> 'b" where 

1105 
"Lim net f = (THE l. (f > l) net)" 

1106 

1107 
lemma Lim: 

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

1109 
trivial_limit net \<or> 

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

1111 
unfolding tendsto_iff trivial_limit_eq by auto 

1112 

1113 

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

1115 

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

1117 
(\<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)" 

1118 
by (auto simp add: tendsto_iff eventually_within_le) 

1119 

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

1121 
(\<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)" 

1122 
by (auto simp add: tendsto_iff eventually_within) 

1123 

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

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

1126 
by (auto simp add: tendsto_iff eventually_at) 

1127 

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

1129 
unfolding Lim_at LIM_def by (simp only: zero_less_dist_iff) 

1130 

1131 
lemma Lim_at_infinity: 

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

1133 
by (auto simp add: tendsto_iff eventually_at_infinity) 

1134 

1135 
lemma Lim_sequentially: 

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

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

1138 
by (auto simp add: tendsto_iff eventually_sequentially) 

1139 

1140 
lemma Lim_sequentially_iff_LIMSEQ: "(S > l) sequentially \<longleftrightarrow> S > l" 

1141 
unfolding Lim_sequentially LIMSEQ_def .. 

1142 

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

1144 
by (rule topological_tendstoI, auto elim: eventually_rev_mono) 

1145 

1146 
text{* The expected monotonicity property. *} 

1147 

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

1149 
unfolding tendsto_def Limits.eventually_within by simp 

1150 

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

1152 
unfolding tendsto_def Limits.eventually_within 

1153 
by (auto elim!: eventually_elim1) 

1154 

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

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

1157 
using assms unfolding tendsto_def Limits.eventually_within 

1158 
apply clarify 

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

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

1161 
apply (auto elim: eventually_elim2) 

1162 
done 

1163 

1164 
lemma Lim_Un_univ: 

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

1166 
==> (f > l) net" 

1167 
by (metis Lim_Un within_UNIV) 

1168 

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

1170 

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

1172 
(* FIXME: rename *) 

1173 
unfolding tendsto_def Limits.eventually_within 

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

1175 
by (auto elim!: eventually_elim1) 

1176 

1177 
lemma Lim_within_open: 

1178 
fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space" 

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

1180 
shows "(f > l)(at a within S) \<longleftrightarrow> (f > l)(at a)" (is "?lhs \<longleftrightarrow> ?rhs") 

1181 
proof 

1182 
assume ?lhs 

1183 
{ fix A assume "open A" "l \<in> A" 

1184 
with `?lhs` have "eventually (\<lambda>x. f x \<in> A) (at a within S)" 

1185 
by (rule topological_tendstoD) 

1186 
hence "eventually (\<lambda>x. x \<in> S \<longrightarrow> f x \<in> A) (at a)" 

1187 
unfolding Limits.eventually_within . 

1188 
then obtain T where "open T" "a \<in> T" "\<forall>x\<in>T. x \<noteq> a \<longrightarrow> x \<in> S \<longrightarrow> f x \<in> A" 

1189 
unfolding eventually_at_topological by fast 

1190 
hence "open (T \<inter> S)" "a \<in> T \<inter> S" "\<forall>x\<in>(T \<inter> S). x \<noteq> a \<longrightarrow> f x \<in> A" 

1191 
using assms by auto 

1192 
hence "\<exists>T. open T \<and> a \<in> T \<and> (\<forall>x\<in>T. x \<noteq> a \<longrightarrow> f x \<in> A)" 

1193 
by fast 

1194 
hence "eventually (\<lambda>x. f x \<in> A) (at a)" 

1195 
unfolding eventually_at_topological . 

1196 
} 

1197 
thus ?rhs by (rule topological_tendstoI) 

1198 
next 

1199 
assume ?rhs 

1200 
thus ?lhs by (rule Lim_at_within) 

1201 
qed 

1202 

1203 
text{* Another limit point characterization. *} 

1204 

1205 
lemma islimpt_sequential: 

1206 
fixes x :: "'a::metric_space" (* FIXME: generalize to topological_space *) 

1207 
shows "x islimpt S \<longleftrightarrow> (\<exists>f. (\<forall>n::nat. f n \<in> S {x}) \<and> (f > x) sequentially)" 

1208 
(is "?lhs = ?rhs") 

1209 
proof 

1210 
assume ?lhs 

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

1212 
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 

1213 
{ fix n::nat 

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

1215 
} 

1216 
moreover 

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

1218 
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 

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

1220 
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) 

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

1222 
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 

1223 
} 

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

1225 
unfolding Lim_sequentially using f by auto 

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

1227 
next 

1228 
assume ?rhs 

1229 
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 

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

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

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

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

1234 
} 

1235 
thus ?lhs unfolding islimpt_approachable by auto 

1236 
qed 

1237 

1238 
text{* Basic arithmetical combining theorems for limits. *} 

1239 

1240 
lemma Lim_linear: 

1241 
assumes "(f > l) net" "bounded_linear h" 

1242 
shows "((\<lambda>x. h (f x)) > h l) net" 

1243 
using `bounded_linear h` `(f > l) net` 

1244 
by (rule bounded_linear.tendsto) 

1245 

1246 
lemma Lim_ident_at: "((\<lambda>x. x) > a) (at a)" 

1247 
unfolding tendsto_def Limits.eventually_at_topological by fast 

1248 

34964  1249 
lemma Lim_const[intro]: "((\<lambda>x. a) > a) net" by (rule tendsto_const) 
1250 

1251 
lemma Lim_cmul[intro]: 

33175  1252 
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" 
1253 
shows "(f > l) net ==> ((\<lambda>x. c *\<^sub>R f x) > c *\<^sub>R l) net" 

1254 
by (intro tendsto_intros) 

1255 

1256 
lemma Lim_neg: 

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

1258 
shows "(f > l) net ==> ((\<lambda>x. (f x)) > l) net" 

1259 
by (rule tendsto_minus) 

1260 

1261 
lemma Lim_add: fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" shows 

1262 
"(f > l) net \<Longrightarrow> (g > m) net \<Longrightarrow> ((\<lambda>x. f(x) + g(x)) > l + m) net" 

1263 
by (rule tendsto_add) 

1264 

1265 
lemma Lim_sub: 

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

1267 
shows "(f > l) net \<Longrightarrow> (g > m) net \<Longrightarrow> ((\<lambda>x. f(x)  g(x)) > l  m) net" 

1268 
by (rule tendsto_diff) 

1269 

1270 
lemma Lim_null: 

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

1272 
shows "(f > l) net \<longleftrightarrow> ((\<lambda>x. f(x)  l) > 0) net" by (simp add: Lim dist_norm) 

1273 

1274 
lemma Lim_null_norm: 

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

1276 
shows "(f > 0) net \<longleftrightarrow> ((\<lambda>x. norm(f x)) > 0) net" 

1277 
by (simp add: Lim dist_norm) 

1278 

1279 
lemma Lim_null_comparison: 

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

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

1282 
shows "(f > 0) net" 

1283 
proof(simp add: tendsto_iff, rule+) 

1284 
fix e::real assume "0<e" 

1285 
{ fix x 

1286 
assume "norm (f x) \<le> g x" "dist (g x) 0 < e" 

1287 
hence "dist (f x) 0 < e" by (simp add: dist_norm) 

1288 
} 

1289 
thus "eventually (\<lambda>x. dist (f x) 0 < e) net" 

1290 
using eventually_and[of "\<lambda>x. norm(f x) <= g x" "\<lambda>x. dist (g x) 0 < e" net] 

1291 
using eventually_mono[of "(\<lambda>x. norm (f x) \<le> g x \<and> dist (g x) 0 < e)" "(\<lambda>x. dist (f x) 0 < e)" net] 

1292 
using assms `e>0` unfolding tendsto_iff by auto 

1293 
qed 

1294 

1295 
lemma Lim_component: 

34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34289
diff
changeset

1296 
fixes f :: "'a \<Rightarrow> 'b::metric_space ^ 'n" 
33175  1297 
shows "(f > l) net \<Longrightarrow> ((\<lambda>a. f a $i) > l$i) net" 
1298 
unfolding tendsto_iff 

1299 
apply (clarify) 

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

1301 
apply (erule eventually_elim1) 

1302 
apply (erule le_less_trans [OF dist_nth_le]) 

1303 
done 

1304 

1305 
lemma Lim_transform_bound: 

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

1307 
fixes g :: "'a \<Rightarrow> 'c::real_normed_vector" 

1308 
assumes "eventually (\<lambda>n. norm(f n) <= norm(g n)) net" "(g > 0) net" 
