author  huffman 
Thu, 25 Aug 2011 09:17:02 0700  
changeset 44519  ea85d78a994e 
parent 44518  219a6fe4cfae 
child 44522  2f7e9d890efe 
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 

44517  10 
imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs" Norm_Arith L2_Norm 
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) 
44457
d366fa5551ef
declare euclidean_simps [simp] at the point they are proved;
huffman
parents:
44365
diff
changeset

17 
by(auto simp add:power2_eq_square) 
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 

44517  23 
subsection {* General notion of a topology as a value *} 
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 

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

560 
lemma interiorI [intro?]: 

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

562 
shows "x \<in> interior S" 

563 
using assms unfolding interior_def by fast 

564 

565 
lemma interiorE [elim?]: 

566 
assumes "x \<in> interior S" 

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

568 
using assms unfolding interior_def by fast 

569 

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

571 
by (simp add: interior_def open_Union) 

572 

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

574 
by (auto simp add: interior_def) 

575 

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

577 
by (auto simp add: interior_def) 

578 

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

580 
by (intro equalityI interior_subset interior_maximal subset_refl) 

33175  581 

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

44519  583 
by (metis open_interior interior_open) 
584 

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

33175  586 
by (metis interior_maximal interior_subset subset_trans) 
587 

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

590 

591 
lemma interior_interior [simp]: "interior (interior S) = interior S" 

592 
using open_interior by (rule interior_open) 

593 

594 
lemma subset_interior: "S \<subseteq> T \<Longrightarrow> interior S \<subseteq> interior T" 

595 
by (auto simp add: interior_def) (* TODO: rename to interior_mono *) 

596 

597 
lemma interior_unique: 

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

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

600 
shows "interior S = T" 

601 
by (intro equalityI assms interior_subset open_interior interior_maximal) 

602 

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

604 
by (intro equalityI Int_mono Int_greatest subset_interior Int_lower1 

605 
Int_lower2 interior_maximal interior_subset open_Int open_interior) 

606 

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

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

609 
by (simp add: open_subset_interior) 

33175  610 

611 
lemma interior_limit_point [intro]: 

612 
fixes x :: "'a::perfect_space" 

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

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

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

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

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

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

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

619 
done 
33175  620 

621 
lemma interior_closed_Un_empty_interior: 

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

44519  623 
shows "interior (S \<union> T) = interior S" 
33175  624 
proof 
44519  625 
show "interior S \<subseteq> interior (S \<union> T)" 
626 
by (rule subset_interior, rule Un_upper1) 

33175  627 
next 
628 
show "interior (S \<union> T) \<subseteq> interior S" 

629 
proof 

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

44519  631 
then obtain R where "open R" "x \<in> R" "R \<subseteq> S \<union> T" .. 
33175  632 
show "x \<in> interior S" 
633 
proof (rule ccontr) 

634 
assume "x \<notin> interior S" 

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

44519  636 
unfolding interior_def by fast 
33175  637 
from `open R` `closed S` have "open (R  S)" by (rule open_Diff) 
638 
from `R \<subseteq> S \<union> T` have "R  S \<subseteq> T" by fast 

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

640 
show "False" unfolding interior_def by fast 

641 
qed 

642 
qed 

643 
qed 

644 

44365  645 
lemma interior_Times: "interior (A \<times> B) = interior A \<times> interior B" 
646 
proof (rule interior_unique) 

647 
show "interior A \<times> interior B \<subseteq> A \<times> B" 

648 
by (intro Sigma_mono interior_subset) 

649 
show "open (interior A \<times> interior B)" 

650 
by (intro open_Times open_interior) 

44519  651 
fix T assume "T \<subseteq> A \<times> B" and "open T" thus "T \<subseteq> interior A \<times> interior B" 
652 
proof (safe) 

653 
fix x y assume "(x, y) \<in> T" 

654 
then obtain C D where "open C" "open D" "C \<times> D \<subseteq> T" "x \<in> C" "y \<in> D" 

655 
using `open T` unfolding open_prod_def by fast 

656 
hence "open C" "open D" "C \<subseteq> A" "D \<subseteq> B" "x \<in> C" "y \<in> D" 

657 
using `T \<subseteq> A \<times> B` by auto 

658 
thus "x \<in> interior A" and "y \<in> interior B" 

659 
by (auto intro: interiorI) 

660 
qed 

44365  661 
qed 
662 

33175  663 

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

664 
subsection {* Closure of a Set *} 
33175  665 

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

667 

44518  668 
lemma interior_closure: "interior S =  (closure ( S))" 
669 
unfolding interior_def closure_def islimpt_def by auto 

670 

34105  671 
lemma closure_interior: "closure S =  interior ( S)" 
44518  672 
unfolding interior_closure by simp 
33175  673 

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

44518  675 
unfolding closure_interior by (simp add: closed_Compl) 
676 

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

678 
unfolding closure_def by simp 

33175  679 

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

44519  681 
unfolding hull_def closure_interior interior_def by auto 
33175  682 

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

44519  684 
unfolding closure_hull using closed_Inter by (rule hull_eq) 
685 

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

687 
unfolding closure_eq . 

688 

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

44518  690 
unfolding closure_hull by (rule hull_hull) 
33175  691 

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

44518  693 
unfolding closure_hull by (rule hull_mono) 
33175  694 

44519  695 
lemma closure_minimal: "S \<subseteq> T \<Longrightarrow> closed T \<Longrightarrow> closure S \<subseteq> T" 
44518  696 
unfolding closure_hull by (rule hull_minimal) 
33175  697 

44519  698 
lemma closure_unique: 
699 
assumes "S \<subseteq> T" and "closed T" 

700 
assumes "\<And>T'. S \<subseteq> T' \<Longrightarrow> closed T' \<Longrightarrow> T \<subseteq> T'" 

701 
shows "closure S = T" 

702 
using assms unfolding closure_hull by (rule hull_unique) 

703 

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

44518  705 
using closed_empty by (rule closure_closed) 
33175  706 

44519  707 
lemma closure_univ [simp]: "closure UNIV = UNIV" 
44518  708 
using closed_UNIV by (rule closure_closed) 
709 

710 
lemma closure_union [simp]: "closure (S \<union> T) = closure S \<union> closure T" 

711 
unfolding closure_interior by simp 

33175  712 

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

714 
using closure_empty closure_subset[of S] 

715 
by blast 

716 

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

718 
using closure_eq[of S] closure_subset[of S] 

719 
by simp 

720 

721 
lemma open_inter_closure_eq_empty: 

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

34105  723 
using open_subset_interior[of S " T"] 
724 
using interior_subset[of " T"] 

33175  725 
unfolding closure_interior 
726 
by auto 

727 

728 
lemma open_inter_closure_subset: 

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

730 
proof 

731 
fix x 

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

733 
{ assume *:"x islimpt T" 

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

735 
proof (rule islimptI) 

736 
fix A 

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

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

739 
by (simp_all add: open_Int) 

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

741 
by (rule islimptE) 

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

743 
by simp_all 

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

745 
qed 

746 
} 

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

748 
unfolding closure_def 

749 
by blast 

750 
qed 

751 

44519  752 
lemma closure_complement: "closure ( S) =  interior S" 
44518  753 
unfolding closure_interior by simp 
33175  754 

44519  755 
lemma interior_complement: "interior ( S) =  closure S" 
44518  756 
unfolding closure_interior by simp 
33175  757 

44365  758 
lemma closure_Times: "closure (A \<times> B) = closure A \<times> closure B" 
44519  759 
proof (rule closure_unique) 
44365  760 
show "A \<times> B \<subseteq> closure A \<times> closure B" 
761 
by (intro Sigma_mono closure_subset) 

762 
show "closed (closure A \<times> closure B)" 

763 
by (intro closed_Times closed_closure) 

44519  764 
fix T assume "A \<times> B \<subseteq> T" and "closed T" thus "closure A \<times> closure B \<subseteq> T" 
44365  765 
apply (simp add: closed_def open_prod_def, clarify) 
766 
apply (rule ccontr) 

767 
apply (drule_tac x="(a, b)" in bspec, simp, clarify, rename_tac C D) 

768 
apply (simp add: closure_interior interior_def) 

769 
apply (drule_tac x=C in spec) 

770 
apply (drule_tac x=D in spec) 

771 
apply auto 

772 
done 

773 
qed 

774 

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

775 

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

776 
subsection {* Frontier (aka boundary) *} 
33175  777 

778 
definition "frontier S = closure S  interior S" 

779 

780 
lemma frontier_closed: "closed(frontier S)" 

781 
by (simp add: frontier_def closed_Diff) 

782 

34105  783 
lemma frontier_closures: "frontier S = (closure S) \<inter> (closure( S))" 
33175  784 
by (auto simp add: frontier_def interior_closure) 
785 

786 
lemma frontier_straddle: 

787 
fixes a :: "'a::metric_space" 

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

789 
proof 

790 
assume "?lhs" 

791 
{ fix e::real 

792 
assume "e > 0" 

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

794 
{ assume "a\<in>S" 

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

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

797 
unfolding frontier_closures closure_def islimpt_def using `e>0` 

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

799 
ultimately have ?rhse by auto 

800 
} 

801 
moreover 

802 
{ assume "a\<notin>S" 

803 
hence ?rhse using `?lhs` 

804 
unfolding frontier_closures closure_def islimpt_def 

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

33324  806 
by simp (metis centre_in_ball mem_ball open_ball) 
33175  807 
} 
808 
ultimately have ?rhse by auto 

809 
} 

810 
thus ?rhs by auto 

811 
next 

812 
assume ?rhs 

813 
moreover 

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

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

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

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

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

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

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

821 
} 

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

823 
moreover 

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

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

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

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

33175  831 
qed 
832 

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

834 
by (metis frontier_def closure_closed Diff_subset) 

835 

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

837 
by (simp add: frontier_def) 
33175  838 

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

840 
proof 

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

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

843 
hence "closed S" using closure_subset_eq by auto 

844 
} 

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

845 
thus ?thesis using frontier_subset_closed[of S] .. 
33175  846 
qed 
847 

34105  848 
lemma frontier_complement: "frontier( S) = frontier S" 
33175  849 
by (auto simp add: frontier_def closure_complement interior_complement) 
850 

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

34105  852 
using frontier_complement frontier_subset_eq[of " S"] 
853 
unfolding open_closed by auto 

33175  854 

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

855 

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

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

857 

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

859 
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

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

862 
definition 

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

863 
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

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

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

867 
text{* Prove That They are all filters. *} 
33175  868 

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

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

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

872 
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

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

874 
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

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

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

877 
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

878 
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

879 
qed auto 
33175  880 

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

883 
lemma trivial_limit_within: 

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

885 
proof 

886 
assume "trivial_limit (at a within S)" 

887 
thus "\<not> a islimpt S" 

888 
unfolding trivial_limit_def 

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

889 
unfolding eventually_within eventually_at_topological 
33175  890 
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

891 
apply (clarsimp simp add: set_eq_iff) 
33175  892 
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

893 
apply (clarsimp, drule_tac x=y in bspec, simp_all) 
33175  894 
done 
895 
next 

896 
assume "\<not> a islimpt S" 

897 
thus "trivial_limit (at a within S)" 

898 
unfolding trivial_limit_def 

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

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

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

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

903 
apply auto 
33175  904 
done 
905 
qed 

906 

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

908 
using trivial_limit_within [of a UNIV] 

909 
by (simp add: within_UNIV) 

910 

911 
lemma trivial_limit_at: 

912 
fixes a :: "'a::perfect_space" 

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

914 
by (simp add: trivial_limit_at_iff) 

915 

916 
lemma trivial_limit_at_infinity: 

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

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

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

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

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

921 
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

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

923 
apply (drule_tac x=UNIV in spec, simp) 
33175  924 
done 
925 

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

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

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

930 
unfolding eventually_at dist_nz by auto 

931 

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

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

934 
unfolding eventually_within eventually_at dist_nz by auto 

935 

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

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

938 
unfolding eventually_within 

33324  939 
by auto (metis Rats_dense_in_nn_real order_le_less_trans order_refl) 
33175  940 

941 
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

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

943 
by (auto elim: eventually_rev_mp) 
33175  944 

945 
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

946 
unfolding trivial_limit_def by (auto elim: eventually_rev_mp) 
33175  947 

948 
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

949 
by (simp add: filter_eq_iff) 
33175  950 

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

952 

953 
lemma eventually_rev_mono: 

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

955 
using eventually_mono [of P Q] by fast 

956 

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

958 
by (simp add: eventually_False) 

959 

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

960 

36437  961 
subsection {* Limits *} 
33175  962 

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

963 
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

964 

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

965 
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

966 
where "Lim A f = (THE l. (f > l) A)" 
33175  967 

968 
lemma Lim: 

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

970 
trivial_limit net \<or> 

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

972 
unfolding tendsto_iff trivial_limit_eq by auto 

973 

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

975 

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

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

978 
by (auto simp add: tendsto_iff eventually_within_le) 

979 

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

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

982 
by (auto simp add: tendsto_iff eventually_within) 

983 

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

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

986 
by (auto simp add: tendsto_iff eventually_at) 

987 

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

989 
unfolding Lim_at LIM_def by (simp only: zero_less_dist_iff) 

990 

991 
lemma Lim_at_infinity: 

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

993 
by (auto simp add: tendsto_iff eventually_at_infinity) 

994 

995 
lemma Lim_sequentially: 

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

997 
(\<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

998 
by (rule LIMSEQ_def) (* FIXME: redundant *) 
33175  999 

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

1001 
by (rule topological_tendstoI, auto elim: eventually_rev_mono) 

1002 

1003 
text{* The expected monotonicity property. *} 

1004 

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

1006 
unfolding tendsto_def Limits.eventually_within by simp 

1007 

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

1009 
unfolding tendsto_def Limits.eventually_within 

1010 
by (auto elim!: eventually_elim1) 

1011 

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

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

1014 
using assms unfolding tendsto_def Limits.eventually_within 

1015 
apply clarify 

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

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

1018 
apply (auto elim: eventually_elim2) 

1019 
done 

1020 

1021 
lemma Lim_Un_univ: 

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

1023 
==> (f > l) net" 

1024 
by (metis Lim_Un within_UNIV) 

1025 

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

1027 

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

1029 
(* FIXME: rename *) 

1030 
unfolding tendsto_def Limits.eventually_within 

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

1032 
by (auto elim!: eventually_elim1) 

1033 

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

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

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

1036 
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

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

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

1040 
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

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

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

1043 
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

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

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

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

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

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

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

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

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

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

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

1054 

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

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

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

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

1058 

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

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

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

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

1062 

33175  1063 
lemma Lim_within_open: 
1064 
fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space" 

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

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

1066 
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

1067 
using assms by (simp only: at_within_open) 
33175  1068 

43338  1069 
lemma Lim_within_LIMSEQ: 
1070 
fixes a :: real and L :: "'a::metric_space" 

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

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

1073 
proof (rule ccontr) 

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

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

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

1077 
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 

1078 

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

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

1081 
using r by (simp add: Bex_def) 

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

1083 
by (rule someI_ex) 

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

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

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

1087 
by fast+ 

1088 

1089 
have "?F > a" 

1090 
proof (rule LIMSEQ_I, unfold real_norm_def) 

1091 
fix e::real 

1092 
assume "0 < e" 

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

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

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

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

1097 
proof (intro exI allI impI) 

1098 
fix n 

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

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

1101 
by (rule F2) 

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

1103 
using mlen by auto 

1104 
also from nodef have 

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

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

1107 
qed 

1108 
qed 

1109 
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` 

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

1111 

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

1113 
proof  

1114 
{ 

1115 
fix no::nat 

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

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

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

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

1120 
by (rule F3) 

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

1122 
} 

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

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

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

1126 
qed 

1127 
ultimately show False by simp 

1128 
qed 

1129 

1130 
lemma Lim_right_bound: 

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

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

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

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

1135 
proof cases 

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

1137 
next 

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

1139 
show ?thesis 

1140 
proof (rule Lim_within_LIMSEQ, safe) 

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

1142 

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

1144 
proof (rule LIMSEQ_I, rule ccontr) 

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

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

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

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

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

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

1151 

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

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

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

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

1156 
by (auto simp: not_less field_simps) 

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

1158 
show False by auto 

1159 
qed 

1160 
qed 

1161 
qed 

1162 

33175  1163 
text{* Another limit point characterization. *} 
1164 

1165 
lemma islimpt_sequential: 

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

1169 
proof 

1170 
assume ?lhs 

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

1172 
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 

1173 
{ fix n::nat 

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

1175 
} 

1176 
moreover 

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

1178 
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 

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

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

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

1182 
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 

1183 
} 

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

1185 
unfolding Lim_sequentially using f by auto 

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

1187 
next 

1188 
assume ?rhs 

1189 
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 

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

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

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

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

1194 
} 

1195 
thus ?lhs unfolding islimpt_approachable by auto 

1196 
qed 

1197 

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

1199 
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

1200 
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

1201 
shows "((inverse o f) > inverse l) A" 
36437  1202 
unfolding o_def using assms by (rule tendsto_inverse) 
1203 

33175  1204 
lemma Lim_null: 
1205 
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" 

44125  1206 
shows "(f > l) net \<longleftrightarrow> ((\<lambda>x. f(x)  l) > 0) net" 
33175  1207 
by (simp add: Lim dist_norm) 
1208 

1209 
lemma Lim_null_comparison: 

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

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

1212 
shows "(f > 0) net" 

44252
10362a07eb7c
Topology_Euclidean_Space.thy: simplify some proofs
huffman
parents:
44250
diff
changeset

1213 
proof (rule metric_tendsto_imp_tendsto) 
10362a07eb7c
Topology_Euclidean_Space.thy: simplify some proofs
huffman
parents:
44250
diff
changeset

1214 
show "(g > 0) net" by fact 