author  huffman 
Mon, 05 Dec 2011 15:10:15 +0100  
changeset 45776  714100f5fda4 
parent 45548  3e2722d66169 
child 46887  cb891d9a23c1 
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 

44628
bd17b7543af1
move lemmas from Topology_Euclidean_Space to Euclidean_Space
huffman
parents:
44584
diff
changeset

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

44517  13 
subsection {* General notion of a topology as a value *} 
33175  14 

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

15 
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

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

19 

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

21 
using openin[of U] by blast 

22 

23 
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

24 
using topology_inverse[unfolded mem_Collect_eq] . 
33175  25 

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

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

28 

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

30 
proof 

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

32 
moreover 

33 
{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

34 
hence "openin T1 = openin T2" by (simp add: fun_eq_iff) 
33175  35 
hence "topology (openin T1) = topology (openin T2)" by simp 
36 
hence "T1 = T2" unfolding openin_inverse .} 

37 
ultimately show ?thesis by blast 

38 
qed 

39 

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

41 

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

43 

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

44 
subsubsection {* Main properties of open sets *} 
33175  45 

46 
lemma openin_clauses: 

47 
fixes U :: "'a topology" 

48 
shows "openin U {}" 

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

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

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

52 
by fast+ 
33175  53 

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

55 
unfolding topspace_def by blast 

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

57 

58 
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

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

60 

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

61 
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

62 
using openin_clauses by simp 
33175  63 

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

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

66 

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

68 

69 
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  70 
proof 
71 
assume ?lhs then show ?rhs by auto 

72 
next 

73 
assume H: ?rhs 

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

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

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

77 
finally show "openin U S" . 

33175  78 
qed 
79 

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

80 
subsubsection {* Closed sets *} 
33175  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 

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

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

122 

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

123 
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

124 

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

125 
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

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

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

129 
{fix A B assume A: "?L A" and B: "?L B" 
33175  130 
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 
131 
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

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

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

135 
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

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

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

140 
obtain Sk where Sk: "Sk \<subseteq> Collect (openin U)" "K = (\<lambda>S. S \<inter> V) ` Sk" by blast 
33175  141 
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

142 
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

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

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

145 
unfolding subset_eq mem_Collect_eq istopology_def by blast 
33175  146 
qed 
147 

148 
lemma openin_subtopology: 

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

150 
unfolding subtopology_def topology_inverse'[OF istopology_subtopology] 

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

151 
by auto 
33175  152 

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

154 
by (auto simp add: topspace_def openin_subtopology) 

155 

156 
lemma closedin_subtopology: 

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

158 
unfolding closedin_def topspace_subtopology 

159 
apply (simp add: openin_subtopology) 

160 
apply (rule iffI) 

161 
apply clarify 

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

163 
by auto 

164 

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

166 
unfolding openin_subtopology 

167 
apply (rule iffI, clarify) 

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

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

170 
by auto 

171 

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

173 
shows "subtopology U V = U" 

174 
proof 

175 
{fix S 

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

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

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

179 
moreover 

180 
{assume S: "openin U S" 

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

182 
using openin_subset[OF S] UV by auto} 

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

184 
then show ?thesis unfolding topology_eq openin_subtopology by blast 

185 
qed 

186 

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

188 
by (simp add: subtopology_superset) 

189 

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

191 
by (simp add: subtopology_superset) 

192 

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

193 
subsubsection {* The standard Euclidean topology *} 
33175  194 

195 
definition 

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

197 
"euclidean = topology open" 

198 

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

200 
unfolding euclidean_def 

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

202 
apply (rule topology_inverse[symmetric]) 

203 
apply (auto simp add: istopology_def) 

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

204 
done 
33175  205 

206 
lemma topspace_euclidean: "topspace euclidean = UNIV" 

207 
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

208 
apply (rule set_eqI) 
33175  209 
by (auto simp add: open_openin[symmetric]) 
210 

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

212 
by (simp add: topspace_euclidean topspace_subtopology) 

213 

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

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

216 

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

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

219 

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

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

221 

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

222 
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

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

224 

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

225 
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

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

227 

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

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

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

230 
by (metis Int_absorb1 openin_open_Int) 
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 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

233 
by (auto simp add: openin_open) 
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 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

236 
by (simp add: closedin_subtopology closed_closedin Int_ac) 
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 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

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

240 

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

241 
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

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

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

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

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

246 

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

247 
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

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

249 

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

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

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

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

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

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

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

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

257 
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

258 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

276 

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

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

278 

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

279 
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

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

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

282 

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

283 
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

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

285 

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

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

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

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

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

290 
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

291 

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

292 
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

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

294 

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

298 
definition 

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

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

301 

302 
definition 

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

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

305 

45776
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

306 
lemma mem_ball [simp]: "y \<in> ball x e \<longleftrightarrow> dist x y < e" 
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

307 
by (simp add: ball_def) 
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

308 

714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

309 
lemma mem_cball [simp]: "y \<in> cball x e \<longleftrightarrow> dist x y \<le> e" 
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

310 
by (simp add: cball_def) 
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

311 

714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

312 
lemma mem_ball_0: 
33175  313 
fixes x :: "'a::real_normed_vector" 
314 
shows "x \<in> ball 0 e \<longleftrightarrow> norm x < e" 

315 
by (simp add: dist_norm) 

316 

45776
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

317 
lemma mem_cball_0: 
33175  318 
fixes x :: "'a::real_normed_vector" 
319 
shows "x \<in> cball 0 e \<longleftrightarrow> norm x \<le> e" 

320 
by (simp add: dist_norm) 

321 

45776
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

322 
lemma centre_in_ball: "x \<in> ball x e \<longleftrightarrow> 0 < e" 
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

323 
by simp 
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

324 

714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

325 
lemma centre_in_cball: "x \<in> cball x e \<longleftrightarrow> 0 \<le> e" 
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

326 
by simp 
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

327 

33175  328 
lemma ball_subset_cball[simp,intro]: "ball x e \<subseteq> cball x e" by (simp add: subset_eq) 
329 
lemma subset_ball[intro]: "d <= e ==> ball x d \<subseteq> ball x e" by (simp add: subset_eq) 

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

331 
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

332 
by (simp add: set_eq_iff) arith 
33175  333 

334 
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

335 
by (simp add: set_eq_iff) 
33175  336 

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

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

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

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

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

342 

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

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

344 
unfolding open_dist ball_def mem_Collect_eq Ball_def 
33175  345 
unfolding dist_commute 
346 
apply clarify 

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

348 
using dist_triangle_alt[where z=x] 

349 
apply (clarsimp simp add: diff_less_iff) 

350 
apply atomize 

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

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

353 
by arith 

354 

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

356 
unfolding open_dist subset_eq mem_ball Ball_def dist_commute .. 

357 

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

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

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

360 
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

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

362 

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

365 

366 
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

367 
unfolding mem_ball set_eq_iff 
33175  368 
apply (simp add: not_less) 
369 
by (metis zero_le_dist order_trans dist_self) 

370 

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

372 

373 

374 
subsection{* Connectedness *} 

375 

376 
definition "connected S \<longleftrightarrow> 

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

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

379 

380 
lemma connected_local: 

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

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

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

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

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

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

387 
~(e2 = {}))" 

388 
unfolding connected_def openin_open by (safe, blast+) 

389 

34105  390 
lemma exists_diff: 
391 
fixes P :: "'a set \<Rightarrow> bool" 

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

33175  393 
proof 
394 
{assume "?lhs" hence ?rhs by blast } 

395 
moreover 

396 
{fix S assume H: "P S" 

34105  397 
have "S =  ( S)" by auto 
398 
with H have "P ( ( S))" by metis } 

33175  399 
ultimately show ?thesis by metis 
400 
qed 

401 

402 
lemma connected_clopen: "connected S \<longleftrightarrow> 

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

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

405 
proof 

34105  406 
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  407 
unfolding connected_def openin_open closedin_closed 
408 
apply (subst exists_diff) by blast 

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

33175  411 

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

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

414 
unfolding connected_def openin_open closedin_closed by auto 

415 
{fix e2 

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

417 
by auto} 

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

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

420 
then show ?thesis unfolding th0 th1 by simp 

421 
qed 

422 

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

424 
by (simp add: connected_def) 

425 

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

426 

33175  427 
subsection{* Limit points *} 
428 

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

429 
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

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

433 
lemma islimptI: 

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

435 
shows "x islimpt S" 

436 
using assms unfolding islimpt_def by auto 

437 

438 
lemma islimptE: 

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

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

441 
using assms unfolding islimpt_def by auto 

442 

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

445 

446 
lemma islimpt_subset: "\<lbrakk>x islimpt S; S \<subseteq> T\<rbrakk> \<Longrightarrow> x islimpt T" 

447 
unfolding islimpt_def by fast 

33175  448 

449 
lemma islimpt_approachable: 

450 
fixes x :: "'a::metric_space" 

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

44584  452 
unfolding islimpt_iff_eventually eventually_at by fast 
33175  453 

454 
lemma islimpt_approachable_le: 

455 
fixes x :: "'a::metric_space" 

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

457 
unfolding islimpt_approachable 

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

460 
by (simp add: Bex_def conj_commute conj_left_commute) 

33175  461 

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

464 

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

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

466 

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

33175  469 

470 
lemma perfect_choose_dist: 

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

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

474 
by (simp add: islimpt_approachable) 

475 

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

477 
unfolding closed_def 

478 
apply (subst open_subopen) 

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

480 
by (metis ComplE ComplI) 
33175  481 

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

483 
unfolding islimpt_def by auto 

484 

485 
lemma finite_set_avoid: 

486 
fixes a :: "'a::metric_space" 

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

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

41863  489 
case 1 thus ?case by (auto intro: zero_less_one) 
33175  490 
next 
491 
case (2 x F) 

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

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

494 
moreover 

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

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

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

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

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

500 
ultimately show ?case by blast 

501 
qed 

502 

503 
lemma islimpt_finite: 

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

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

506 
unfolding islimpt_approachable 

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

508 

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

510 
apply (rule iffI) 

511 
defer 

512 
apply (metis Un_upper1 Un_upper2 islimpt_subset) 

513 
unfolding islimpt_def 

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

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

516 
apply (auto simp add: open_Int) 

517 
done 

518 

519 
lemma discrete_imp_closed: 

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

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

522 
shows "closed S" 

523 
proof 

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

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

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

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

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

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

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

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

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

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

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

535 
qed 

536 

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

537 

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

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

539 

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

542 
lemma interiorI [intro?]: 

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

544 
shows "x \<in> interior S" 

545 
using assms unfolding interior_def by fast 

546 

547 
lemma interiorE [elim?]: 

548 
assumes "x \<in> interior S" 

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

550 
using assms unfolding interior_def by fast 

551 

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

553 
by (simp add: interior_def open_Union) 

554 

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

556 
by (auto simp add: interior_def) 

557 

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

559 
by (auto simp add: interior_def) 

560 

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

562 
by (intro equalityI interior_subset interior_maximal subset_refl) 

33175  563 

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

44519  565 
by (metis open_interior interior_open) 
566 

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

33175  568 
by (metis interior_maximal interior_subset subset_trans) 
569 

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

572 

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

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

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

575 

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

578 

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

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

580 
by (auto simp add: interior_def) 
44519  581 

582 
lemma interior_unique: 

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

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

585 
shows "interior S = T" 

586 
by (intro equalityI assms interior_subset open_interior interior_maximal) 

587 

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

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

589 
by (intro equalityI Int_mono Int_greatest interior_mono Int_lower1 
44519  590 
Int_lower2 interior_maximal interior_subset open_Int open_interior) 
591 

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

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

594 
by (simp add: open_subset_interior) 

33175  595 

596 
lemma interior_limit_point [intro]: 

597 
fixes x :: "'a::perfect_space" 

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

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

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

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

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

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

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

604 
done 
33175  605 

606 
lemma interior_closed_Un_empty_interior: 

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

44519  608 
shows "interior (S \<union> T) = interior S" 
33175  609 
proof 
44519  610 
show "interior S \<subseteq> interior (S \<union> T)" 
44522
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44519
diff
changeset

611 
by (rule interior_mono, rule Un_upper1) 
33175  612 
next 
613 
show "interior (S \<union> T) \<subseteq> interior S" 

614 
proof 

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

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

619 
assume "x \<notin> interior S" 

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

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

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

625 
show "False" unfolding interior_def by fast 

626 
qed 

627 
qed 

628 
qed 

629 

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

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

633 
by (intro Sigma_mono interior_subset) 

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

635 
by (intro open_Times open_interior) 

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

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

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

640 
using `open T` unfolding open_prod_def by fast 

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

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

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

644 
by (auto intro: interiorI) 

645 
qed 

44365  646 
qed 
647 

33175  648 

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

649 
subsection {* Closure of a Set *} 
33175  650 

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

652 

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

655 

34105  656 
lemma closure_interior: "closure S =  interior ( S)" 
44518  657 
unfolding interior_closure by simp 
33175  658 

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

44518  660 
unfolding closure_interior by (simp add: closed_Compl) 
661 

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

663 
unfolding closure_def by simp 

33175  664 

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

44519  666 
unfolding hull_def closure_interior interior_def by auto 
33175  667 

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

44519  669 
unfolding closure_hull using closed_Inter by (rule hull_eq) 
670 

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

672 
unfolding closure_eq . 

673 

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

44518  675 
unfolding closure_hull by (rule hull_hull) 
33175  676 

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

677 
lemma closure_mono: "S \<subseteq> T \<Longrightarrow> closure S \<subseteq> closure T" 
44518  678 
unfolding closure_hull by (rule hull_mono) 
33175  679 

44519  680 
lemma closure_minimal: "S \<subseteq> T \<Longrightarrow> closed T \<Longrightarrow> closure S \<subseteq> T" 
44518  681 
unfolding closure_hull by (rule hull_minimal) 
33175  682 

44519  683 
lemma closure_unique: 
684 
assumes "S \<subseteq> T" and "closed T" 

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

686 
shows "closure S = T" 

687 
using assms unfolding closure_hull by (rule hull_unique) 

688 

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

44518  690 
using closed_empty by (rule closure_closed) 
33175  691 

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

692 
lemma closure_UNIV [simp]: "closure UNIV = UNIV" 
44518  693 
using closed_UNIV by (rule closure_closed) 
694 

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

696 
unfolding closure_interior by simp 

33175  697 

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

699 
using closure_empty closure_subset[of S] 

700 
by blast 

701 

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

703 
using closure_eq[of S] closure_subset[of S] 

704 
by simp 

705 

706 
lemma open_inter_closure_eq_empty: 

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

34105  708 
using open_subset_interior[of S " T"] 
709 
using interior_subset[of " T"] 

33175  710 
unfolding closure_interior 
711 
by auto 

712 

713 
lemma open_inter_closure_subset: 

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

715 
proof 

716 
fix x 

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

718 
{ assume *:"x islimpt T" 

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

720 
proof (rule islimptI) 

721 
fix A 

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

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

724 
by (simp_all add: open_Int) 

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

726 
by (rule islimptE) 

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

728 
by simp_all 

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

730 
qed 

731 
} 

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

733 
unfolding closure_def 

734 
by blast 

735 
qed 

736 

44519  737 
lemma closure_complement: "closure ( S) =  interior S" 
44518  738 
unfolding closure_interior by simp 
33175  739 

44519  740 
lemma interior_complement: "interior ( S) =  closure S" 
44518  741 
unfolding closure_interior by simp 
33175  742 

44365  743 
lemma closure_Times: "closure (A \<times> B) = closure A \<times> closure B" 
44519  744 
proof (rule closure_unique) 
44365  745 
show "A \<times> B \<subseteq> closure A \<times> closure B" 
746 
by (intro Sigma_mono closure_subset) 

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

748 
by (intro closed_Times closed_closure) 

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

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

753 
apply (simp add: closure_interior interior_def) 

754 
apply (drule_tac x=C in spec) 

755 
apply (drule_tac x=D in spec) 

756 
apply auto 

757 
done 

758 
qed 

759 

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

760 

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

761 
subsection {* Frontier (aka boundary) *} 
33175  762 

763 
definition "frontier S = closure S  interior S" 

764 

765 
lemma frontier_closed: "closed(frontier S)" 

766 
by (simp add: frontier_def closed_Diff) 

767 

34105  768 
lemma frontier_closures: "frontier S = (closure S) \<inter> (closure( S))" 
33175  769 
by (auto simp add: frontier_def interior_closure) 
770 

771 
lemma frontier_straddle: 

772 
fixes a :: "'a::metric_space" 

44909  773 
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))" 
774 
unfolding frontier_def closure_interior 

775 
by (auto simp add: mem_interior subset_eq ball_def) 

33175  776 

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

778 
by (metis frontier_def closure_closed Diff_subset) 

779 

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

781 
by (simp add: frontier_def) 
33175  782 

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

784 
proof 

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

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

787 
hence "closed S" using closure_subset_eq by auto 

788 
} 

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

789 
thus ?thesis using frontier_subset_closed[of S] .. 
33175  790 
qed 
791 

34105  792 
lemma frontier_complement: "frontier( S) = frontier S" 
33175  793 
by (auto simp add: frontier_def closure_complement interior_complement) 
794 

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

34105  796 
using frontier_complement frontier_subset_eq[of " S"] 
797 
unfolding open_closed by auto 

33175  798 

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

799 

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

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

801 

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

803 
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

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

806 
definition 

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

807 
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

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

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

811 
text{* Prove That They are all filters. *} 
33175  812 

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

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

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

816 
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

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

818 
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

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

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

821 
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

822 
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

823 
qed auto 
33175  824 

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

827 
lemma trivial_limit_within: 

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

829 
proof 

830 
assume "trivial_limit (at a within S)" 

831 
thus "\<not> a islimpt S" 

832 
unfolding trivial_limit_def 

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

833 
unfolding eventually_within eventually_at_topological 
33175  834 
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

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

837 
apply (clarsimp, drule_tac x=y in bspec, simp_all) 
33175  838 
done 
839 
next 

840 
assume "\<not> a islimpt S" 

841 
thus "trivial_limit (at a within S)" 

842 
unfolding trivial_limit_def 

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

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

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

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

847 
apply auto 
33175  848 
done 
849 
qed 

850 

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

45031  852 
using trivial_limit_within [of a UNIV] by simp 
33175  853 

854 
lemma trivial_limit_at: 

855 
fixes a :: "'a::perfect_space" 

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

44571  857 
by (rule at_neq_bot) 
33175  858 

859 
lemma trivial_limit_at_infinity: 

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

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

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

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

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

864 
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

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

866 
apply (drule_tac x=UNIV in spec, simp) 
33175  867 
done 
868 

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

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

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

873 
unfolding eventually_at dist_nz by auto 

874 

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

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

877 
unfolding eventually_within eventually_at dist_nz by auto 

878 

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

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

881 
unfolding eventually_within 

44668  882 
by auto (metis dense order_le_less_trans) 
33175  883 

884 
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

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

886 
by (auto elim: eventually_rev_mp) 
33175  887 

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

45031  889 
by simp 
33175  890 

891 
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

892 
by (simp add: filter_eq_iff) 
33175  893 

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

895 

896 
lemma eventually_rev_mono: 

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

898 
using eventually_mono [of P Q] by fast 

899 

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

901 
by (simp add: eventually_False) 

902 

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

903 

36437  904 
subsection {* Limits *} 
33175  905 

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

906 
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

907 

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

908 
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

909 
where "Lim A f = (THE l. (f > l) A)" 
33175  910 

911 
lemma Lim: 

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

913 
trivial_limit net \<or> 

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

915 
unfolding tendsto_iff trivial_limit_eq by auto 

916 

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

918 

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

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

921 
by (auto simp add: tendsto_iff eventually_within_le) 

922 

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

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

925 
by (auto simp add: tendsto_iff eventually_within) 

926 

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

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

929 
by (auto simp add: tendsto_iff eventually_at) 

930 

931 
lemma Lim_at_infinity: 

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

933 
by (auto simp add: tendsto_iff eventually_at_infinity) 

934 

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

936 
by (rule topological_tendstoI, auto elim: eventually_rev_mono) 

937 

938 
text{* The expected monotonicity property. *} 

939 

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

941 
unfolding tendsto_def Limits.eventually_within by simp 

942 

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

944 
unfolding tendsto_def Limits.eventually_within 

945 
by (auto elim!: eventually_elim1) 

946 

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

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

949 
using assms unfolding tendsto_def Limits.eventually_within 

950 
apply clarify 

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

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

953 
apply (auto elim: eventually_elim2) 

954 
done 

955 

956 
lemma Lim_Un_univ: 

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

958 
==> (f > l) net" 

959 
by (metis Lim_Un within_UNIV) 

960 

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

962 

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

964 
(* FIXME: rename *) 

965 
unfolding tendsto_def Limits.eventually_within 

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

967 
by (auto elim!: eventually_elim1) 

968 

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

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

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

971 
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

972 
proof 
44519  973 
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

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

975 
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

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

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

978 
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

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

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

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

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

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

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

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

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

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

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

989 

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

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

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

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

993 

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

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

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

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

997 

33175  998 
lemma Lim_within_open: 
999 
fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space" 

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

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

1001 
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

1002 
using assms by (simp only: at_within_open) 
33175  1003 

43338  1004 
lemma Lim_within_LIMSEQ: 
44584  1005 
fixes a :: "'a::metric_space" 
43338  1006 
assumes "\<forall>S. (\<forall>n. S n \<noteq> a \<and> S n \<in> T) \<and> S > a \<longrightarrow> (\<lambda>n. X (S n)) > L" 
1007 
shows "(X > L) (at a within T)" 

44584  1008 
using assms unfolding tendsto_def [where l=L] 
1009 
by (simp add: sequentially_imp_eventually_within) 

43338  1010 

1011 
lemma Lim_right_bound: 

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

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

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

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

1016 
proof cases 

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

1018 
next 

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

1020 
show ?thesis 

1021 
proof (rule Lim_within_LIMSEQ, safe) 

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

1023 

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

1025 
proof (rule LIMSEQ_I, rule ccontr) 

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

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

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

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

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

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

1032 

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

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

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

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

1037 
by (auto simp: not_less field_simps) 

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

1039 
show False by auto 

1040 
qed 

1041 
qed 

1042 
qed 

1043 

33175  1044 
text{* Another limit point characterization. *} 
1045 

1046 
lemma islimpt_sequential: 

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

1050 
proof 

1051 
assume ?lhs 

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

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

1055 
let ?I = "\<lambda>n. inverse (real (Suc n))" 

1056 
have "\<forall>n. f (?I n) \<in> S  {x}" using f by simp 

1057 
moreover have "(\<lambda>n. f (?I n)) > x" 

1058 
proof (rule metric_tendsto_imp_tendsto) 

1059 
show "?I > 0" 

1060 
by (rule LIMSEQ_inverse_real_of_nat) 

1061 
show "eventually (\<lambda>n. dist (f (?I n)) x \<le> dist (?I n) 0) sequentially" 

1062 
by (simp add: norm_conv_dist [symmetric] less_imp_le f) 

1063 
qed 

1064 
ultimately show ?rhs by fast 

33175  1065 
next 
1066 
assume ?rhs 

44907
93943da0a010
remove redundant lemma Lim_sequentially in favor of lemma LIMSEQ_def
huffman
parents:
44905
diff
changeset

1067 
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 LIMSEQ_def by auto 
33175  1068 
{ fix e::real assume "e>0" 
1069 
then obtain N where "dist (f N) x < e" using f(2) by auto 

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

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

1072 
} 

1073 
thus ?lhs unfolding islimpt_approachable by auto 

1074 
qed 

1075 

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

1077 
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

1078 
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

1079 
shows "((inverse o f) > inverse l) A" 
36437  1080 
unfolding o_def using assms by (rule tendsto_inverse) 
1081 

33175  1082 
lemma Lim_null: 
1083 
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" 

44125  1084 
shows "(f > l) net \<longleftrightarrow> ((\<lambda>x. f(x)  l) > 0) net" 
33175  1085 
by (simp add: Lim dist_norm) 
1086 

1087 
lemma Lim_null_comparison: 

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

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

1090 
shows "(f > 0) net" 

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

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

1092 
show "(g > 0) net" by fact 
10362a07eb7c
Topology_Euclidean_Space.thy: simplify some proofs
huffman
parents:
44250
diff
changeset

1093 
show "eventually (\<lambda>x. dist (f x) 0 \<le> dist (g x) 0) net" 
10362a07eb7c
Topology_Euclidean_Space.thy: simplify some proofs
huffman
parents:
44250
diff
changeset

1094 
using assms(1) by (rule eventually_elim1, simp add: dist_norm) 
33175  1095 
qed 
1096 

1097 
lemma Lim_transform_bound: 

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

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

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

1101 
shows "(f > 0) net" 

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

1102 
using assms(1) tendsto_norm_zero [OF assms(2)] 
10362a07eb7c
Topology_Euclidean_Space.thy: simplify some proofs
huffman
parents:
44250
diff
changeset

1103 
by (rule Lim_null_comparison) 
33175  1104 

1105 
text{* Deducing things about the limit from the elements. *} 

1106 

1107 
lemma Lim_in_closed_set: 

1108 
assumes "closed S" "eventually (\<lambda>x. f(x) \<in> S) net" "\<not>(trivial_limit net)" "(f > l) net" 

1109 
shows "l \<in> S" 

1110 
proof (rule ccontr) 

1111 
assume "l \<notin> S" 

1112 
with `closed S` have "open ( S)" "l \<in>  S" 

1113 
by (simp_all add: open_Compl) 

1114 
with assms(4) have "eventually (\<lambda>x. f x \<in>  S) net" 

1115 
by (rule topological_tendstoD) 

1116 
with assms(2) have "eventually (\<lambda>x. False) net" 

1117 
by (rule eventually_elim2) simp 

1118 
with assms(3) show "False" 

1119 
by (simp add: eventually_False) 

1120 
qed 

1121 

1122 
text{* Need to prove closed(cball(x,e)) before deducing this as a corollary. *} 

1123 

1124 
lemma Lim_dist_ubound: 

1125 
assumes "\<not>(trivial_limit net)" "(f > l) net" "eventually (\<lambda>x. dist a (f x) <= e) net" 

1126 
shows "dist a l <= e" 

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

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

1128 
have "dist a l \<in> {..e}" 
10362a07eb7c
Topology_Euclidean_Space.thy: simplify some proofs
huffman
parents:
44250
diff
changeset

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

1130 
show "closed {..e}" by simp 
10362a07eb7c
Topology_Euclidean_Space.thy: simplify some proofs
huffman
parents:
44250
diff
changeset

1131 
show "eventually (\<lambda>x. dist a (f x) \<in> {..e}) net" by (simp add: assms) 
10362a07eb7c
Topology_Euclidean_Space.thy: simplify some proofs
huffman
parents:
44250
diff
changeset

1132 
show "\<not> trivial_limit net" by fact 
10362a07eb7c
Topology_Euclidean_Space.thy: simplify some proofs
huffman
parents:
44250
diff
changeset

1133 
show "((\<lambda>x. dist a (f x)) > dist a l) net" by (intro tendsto_intros assms) 
10362a07eb7c
Topology_Euclidean_Space.thy: simplify some proofs
huffman
parents:
44250
diff
changeset

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

1135 
thus ?thesis by simp 
33175  1136 
qed 
1137 

1138 
lemma Lim_norm_ubound: 

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

1140 
assumes "\<not>(trivial_limit net)" "(f > l) net" "eventually (\<lambda>x. norm(f x) <= e) net" 

1141 
shows "norm(l) <= e" 

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

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

1143 
have "norm l \<in> {..e}" 
10362a07eb7c
Topology_Euclidean_Space.thy: simplify some proofs
huffman
parents:
44250
diff
changeset

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

1145 
show "closed {..e}" by simp 
10362a07eb7c
Topology_Euclidean_Space.thy: simplify some proofs
huffman
parents:
44250
diff
changeset

1146 
show "eventually (\<lambda>x. norm (f x) \<in> {..e}) net" by (simp add: assms) 
10362a07eb7c
Topology_Euclidean_Space.thy: simplify some proofs
huffman
parents:
44250
diff
changeset

1147 
show "\<not> trivial_limit net" by fact 
10362a07eb7c
Topology_Euclidean_Space.thy: simplify some proofs
huffman
parents:
44250
diff
changeset

1148 
show "((\<lambda>x. norm (f x)) > norm l) net" by (intro tendsto_intros assms) 
10362a07eb7c
Topology_Euclidean_Space.thy: simplify some proofs
huffman
parents:
44250
diff
changeset

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

1150 
thus ?thesis by simp 
33175  1151 
qed 
1152 

1153 
lemma Lim_norm_lbound: 

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

1155 
assumes "\<not> (trivial_limit net)" "(f > l) net" "eventually (\<lambda>x. e <= norm(f x)) net" 

1156 
shows "e \<le> norm l" 

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

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

1158 
have "norm l \<in> {e..}" 
10362a07eb7c
Topology_Euclidean_Space.thy: simplify some proofs
huffman
parents:
44250
diff
changeset

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

1160 
show "closed {e..}" by simp 
10362a07eb7c
Topology_Euclidean_Space.thy: simplify some proofs
huffman
parents:
44250
diff
changeset

1161 
show "eventually (\<lambda>x. norm (f x) \<in> {e..}) net" by (simp add: assms) 
10362a07eb7c
Topology_Euclidean_Space.thy: simplify some proofs
huffman
parents:
44250
diff
changeset

1162 
show "\<not> trivial_limit net" by fact 
10362a07eb7c
Topology_Euclidean_Space.thy: simplify some proofs
huffman
parents:
44250
diff
changeset

1163 
show "((\<lambda>x. norm (f x)) > norm l) net" by (intro tendsto_intros assms) 
10362a07eb7c
Topology_Euclidean_Space.thy: simplify some proofs
huffman
parents:
44250
diff
changeset

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

1165 
thus ?thesis by simp 
33175  1166 
qed 
1167 

1168 
text{* Uniqueness of the limit, when nontrivial. *} 

1169 

1170 
lemma tendsto_Lim: 

1171 
fixes f :: "'a \<Rightarrow> 'b::t2_space" 

1172 
shows "~(trivial_limit net) \<Longrightarrow> (f > l) net ==> Lim net f = l" 

41970  1173 
unfolding Lim_def using tendsto_unique[of net f] by auto 
33175  1174 

1175 
text{* Limit under bilinear function *} 

1176 

1177 
lemma Lim_bilinear: 

1178 
assumes "(f > l) net" and "(g > m) net" and "bounded_bilinear h" 

1179 
shows "((\<lambda>x. h (f x) (g x)) > (h l m)) net" 

1180 
using `bounded_bilinear h` `(f > l) net` `(g > m) net` 

1181 
by (rule bounded_bilinear.tendsto) 

1182 

1183 
text{* These are special for limits out of the same vector space. *} 

1184 

1185 
lemma Lim_within_id: "(id > a) (at a within s)" 

45031  1186 
unfolding id_def by (rule tendsto_ident_at_within) 
33175  1187 

1188 
lemma Lim_at_id: "(id > a) (at a)" 

45031  1189 
unfolding id_def by (rule tendsto_ident_at) 
33175  1190 

1191 
lemma Lim_at_zero: 

1192 
fixes a :: "'a::real_normed_vector" 

1193 
fixes l :: "'b::topological_space" 

1194 
shows "(f > l) (at a) \<longleftrightarrow> ((\<lambda>x. f(a + x)) > l) (at 0)" (is "?lhs = ?rhs") 

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

1195 
using LIM_offset_zero LIM_offset_zero_cancel .. 
33175  1196 

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

1197 
text{* It's also sometimes useful to extract the limit point from the filter. *} 
33175  1198 

1199 
definition 

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

1200 
netlimit :: "'a::t2_space filter \<Rightarrow> 'a" where 
33175  1201 
"netlimit net = (SOME a. ((\<lambda>x. x) > a) net)" 
1202 

1203 
lemma netlimit_within: 

1204 
assumes "\<not> trivial_limit (at a within S)" 

1205 
shows "netlimit (at a within S) = a" 

1206 
unfolding netlimit_def 

1207 
apply (rule some_equality) 

1208 
apply (rule Lim_at_within) 

44568
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44533
diff
changeset

1209 
apply (rule tendsto_ident_at) 
41970  1210 
apply (erule tendsto_unique [OF assms]) 
33175 