33175

1 
(* Title: HOL/Library/Topology_Euclidian_Space.thy


2 
Author: Amine Chaieb, University of Cambridge


3 
Author: Robert Himmelmann, TU Muenchen


4 
*)


5 


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


7 


8 
theory Topology_Euclidean_Space


9 
imports SEQ Euclidean_Space Product_Vector


10 
begin


11 


12 
declare fstcart_pastecart[simp] sndcart_pastecart[simp]


13 


14 
subsection{* General notion of a topology *}


15 


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


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


18 
morphisms "openin" "topology"


19 
unfolding istopology_def by blast


20 


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


22 
using openin[of U] by blast


23 


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


25 
using topology_inverse[unfolded mem_def Collect_def] .


26 


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


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


29 


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


31 
proof


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


33 
moreover


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


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


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


37 
hence "T1 = T2" unfolding openin_inverse .}


38 
ultimately show ?thesis by blast


39 
qed


40 


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


42 


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


44 


45 
subsection{* Main properties of open sets *}


46 


47 
lemma openin_clauses:


48 
fixes U :: "'a topology"


49 
shows "openin U {}"


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


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


52 
using openin[of U] unfolding istopology_def Collect_def mem_def


53 
by (metis mem_def subset_eq)+


54 


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


56 
unfolding topspace_def by blast


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


58 


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


60 
by (simp add: openin_clauses)


61 


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


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


70 
proof


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


72 
moreover


73 
{assume H: ?rhs


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


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


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


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


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


79 
ultimately show ?thesis by blast


80 
qed


81 


82 
subsection{* Closed sets *}


83 


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


85 


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


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


88 
lemma closedin_topspace[intro,simp]:


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


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


91 
by (auto simp add: Diff_Un closedin_def)


92 


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


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


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


96 


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


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


99 


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


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


102 
apply (auto simp add: closedin_def Diff_Diff_Int inf_absorb2)


103 
apply (metis openin_subset subset_eq)


104 
done


105 


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


107 
by (simp add: openin_closedin_eq)


108 


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


110 
proof


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


112 
by (auto simp add: topspace_def openin_subset)


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


114 
qed


115 


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


117 
proof


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


119 
by (auto simp add: topspace_def )


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


121 
qed


122 


123 
subsection{* Subspace topology. *}


124 


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


126 


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


128 
proof


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


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


131 
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


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


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


134 
moreover


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


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


137 
apply (rule set_ext)


138 
apply (simp add: Ball_def image_iff)


139 
by (metis mem_def)


140 
from K[unfolded th0 subset_image_iff]


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


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


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


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


145 
ultimately show ?thesis unfolding istopology_def by blast


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]


151 
by (auto simp add: Collect_def)


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 


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


189 
by (simp add: subtopology_superset)


190 


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


192 
by (simp add: subtopology_superset)


193 


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


195 


196 
definition


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


198 
"euclidean = topology open"


199 


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


201 
unfolding euclidean_def


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


203 
apply (rule topology_inverse[symmetric])


204 
apply (auto simp add: istopology_def)


205 
by (auto simp add: mem_def subset_eq)


206 


207 
lemma topspace_euclidean: "topspace euclidean = UNIV"


208 
apply (simp add: topspace_def)


209 
apply (rule set_ext)


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


211 


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


213 
by (simp add: topspace_euclidean topspace_subtopology)


214 


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


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


217 


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


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


220 


221 
subsection{* Open and closed balls. *}


222 


223 
definition


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


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


226 


227 
definition


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


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


230 


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


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


233 


234 
lemma mem_ball_0 [simp]:


235 
fixes x :: "'a::real_normed_vector"


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


237 
by (simp add: dist_norm)


238 


239 
lemma mem_cball_0 [simp]:


240 
fixes x :: "'a::real_normed_vector"


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


242 
by (simp add: dist_norm)


243 


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


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


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


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


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


249 
by (simp add: expand_set_eq) arith


250 


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


252 
by (simp add: expand_set_eq)


253 


254 
subsection{* Topological properties of open balls *}


255 


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


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


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


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


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


261 


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


263 
unfolding open_dist ball_def Collect_def Ball_def mem_def


264 
unfolding dist_commute


265 
apply clarify


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


267 
using dist_triangle_alt[where z=x]


268 
apply (clarsimp simp add: diff_less_iff)


269 
apply atomize


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


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


272 
by arith


273 


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


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


276 
unfolding open_dist subset_eq mem_ball Ball_def dist_commute ..


277 


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


279 
by (metis open_contains_ball subset_eq centre_in_ball)


280 


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


282 
unfolding mem_ball expand_set_eq


283 
apply (simp add: not_less)


284 
by (metis zero_le_dist order_trans dist_self)


285 


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


287 


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


289 


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


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


292 


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


294 
by (auto simp add: openin_open)


295 


296 
lemma open_openin_trans[trans]:


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


298 
by (metis Int_absorb1 openin_open_Int)


299 


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


301 
by (auto simp add: openin_open)


302 


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


304 
by (simp add: closedin_subtopology closed_closedin Int_ac)


305 


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


307 
by (metis closedin_closed)


308 


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


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


311 
apply auto


312 
apply (frule closedin_closed_Int[of T S])


313 
by simp


314 


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


316 
by (auto simp add: closedin_closed)


317 


318 
lemma openin_euclidean_subtopology_iff:


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


320 
shows "openin (subtopology euclidean U) S


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


322 
proof


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


324 
by (simp add: open_dist) blast}


325 
moreover


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


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


328 
by metis


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


330 
have oT: "open ?T" by auto


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


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


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


334 
by (rule d [THEN conjunct1])


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


336 
moreover


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


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


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


340 
assume "y\<in>U"


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


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


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


344 
ultimately show ?thesis by blast


345 
qed


346 


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


348 


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


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


351 
unfolding open_openin openin_open by blast


352 


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


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


355 


356 
lemma closedin_trans[trans]:


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


358 
closedin (subtopology euclidean U) T


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


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


361 


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


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


364 


365 
subsection{* Connectedness *}


366 


367 
definition "connected S \<longleftrightarrow>


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


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


370 


371 
lemma connected_local:


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


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


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


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


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


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


378 
~(e2 = {}))"


379 
unfolding connected_def openin_open by (safe, blast+)


380 


381 
lemma exists_diff: "(\<exists>S. P(UNIV  S)) \<longleftrightarrow> (\<exists>S. P S)" (is "?lhs \<longleftrightarrow> ?rhs")


382 
proof


383 


384 
{assume "?lhs" hence ?rhs by blast }


385 
moreover


386 
{fix S assume H: "P S"


387 
have "S = UNIV  (UNIV  S)" by auto


388 
with H have "P (UNIV  (UNIV  S))" by metis }


389 
ultimately show ?thesis by metis


390 
qed


391 


392 
lemma connected_clopen: "connected S \<longleftrightarrow>


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


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


395 
proof


396 
have " \<not> connected S \<longleftrightarrow> (\<exists>e1 e2. open e1 \<and> open (UNIV  e2) \<and> S \<subseteq> e1 \<union> (UNIV  e2) \<and> e1 \<inter> (UNIV  e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (UNIV  e2) \<inter> S \<noteq> {})"


397 
unfolding connected_def openin_open closedin_closed


398 
apply (subst exists_diff) by blast


399 
hence th0: "connected S \<longleftrightarrow> \<not> (\<exists>e2 e1. closed e2 \<and> open e1 \<and> S \<subseteq> e1 \<union> (UNIV  e2) \<and> e1 \<inter> (UNIV  e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (UNIV  e2) \<inter> S \<noteq> {})"


400 
(is " _ \<longleftrightarrow> \<not> (\<exists>e2 e1. ?P e2 e1)") apply (simp add: closed_def Compl_eq_Diff_UNIV) by metis


401 


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


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


404 
unfolding connected_def openin_open closedin_closed by auto


405 
{fix e2


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


407 
by auto}


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


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


410 
then show ?thesis unfolding th0 th1 by simp


411 
qed


412 


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


414 
by (simp add: connected_def)


415 


416 
subsection{* Hausdorff and other separation properties *}


417 


418 
class t0_space =


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


420 


421 
class t1_space =


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


423 
begin


424 


425 
subclass t0_space


426 
proof


427 
qed (fast dest: t1_space)


428 


429 
end


430 


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


432 


433 
class t2_space =


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


435 
begin


436 


437 
subclass t1_space


438 
proof


439 
qed (fast dest: hausdorff)


440 


441 
end


442 


443 
instance metric_space \<subseteq> t2_space


444 
proof


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


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


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


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


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


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


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


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


453 
by (auto simp add: expand_set_eq)


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


455 
by blast


456 
qed


457 


458 
lemma separation_t2:


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


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


461 
using hausdorff[of x y] by blast


462 


463 
lemma separation_t1:


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


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


466 
using t1_space[of x y] by blast


467 


468 
lemma separation_t0:


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


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


471 
using t0_space[of x y] by blast


472 


473 
subsection{* Limit points *}


474 


475 
definition


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


477 
(infixr "islimpt" 60) where


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


479 


480 
lemma islimptI:


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


482 
shows "x islimpt S"


483 
using assms unfolding islimpt_def by auto


484 


485 
lemma islimptE:


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


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


488 
using assms unfolding islimpt_def by auto


489 


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


491 


492 
lemma islimpt_approachable:


493 
fixes x :: "'a::metric_space"


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


495 
unfolding islimpt_def


496 
apply auto


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


498 
apply auto


499 
apply(rule_tac x=y in bexI)


500 
apply (auto simp add: dist_commute)


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


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


503 
done


504 


505 
lemma islimpt_approachable_le:


506 
fixes x :: "'a::metric_space"


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


508 
unfolding islimpt_approachable


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


510 
by metis (* FIXME: VERY slow! *)


511 


512 
class perfect_space =


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


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


515 


516 
lemma perfect_choose_dist:


517 
fixes x :: "'a::perfect_space"


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


519 
using islimpt_UNIV [of x]


520 
by (simp add: islimpt_approachable)


521 


522 
instance real :: perfect_space


523 
apply default


524 
apply (rule islimpt_approachable [THEN iffD2])


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


526 
apply (auto simp add: dist_norm)


527 
done


528 


529 
instance "^" :: (perfect_space, finite) perfect_space


530 
proof


531 
fix x :: "'a ^ 'b"


532 
{


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


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


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


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


537 
unfolding islimpt_approachable by auto


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


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


540 
unfolding a_def y_def by (simp add: Cart_eq)


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


542 
unfolding dist_vector_def a_def y_def


543 
apply simp


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


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


546 
done


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


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


549 
}


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


551 
qed


552 


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


554 
unfolding closed_def


555 
apply (subst open_subopen)


556 
apply (simp add: islimpt_def subset_eq Compl_eq_Diff_UNIV)


557 
by (metis DiffE DiffI UNIV_I insertCI insert_absorb mem_def)


558 


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


560 
unfolding islimpt_def by auto


561 


562 
lemma closed_positive_orthant: "closed {x::real^'n::finite. \<forall>i. 0 \<le>x$i}"


563 
proof


564 
let ?U = "UNIV :: 'n set"


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


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


567 
and xi: "x$i < 0"


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


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


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


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


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


573 
apply (simp only: vector_component)


574 
by (rule th') auto


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


576 
apply (simp add: dist_norm) by norm


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


578 
then show ?thesis unfolding closed_limpt islimpt_approachable


579 
unfolding not_le[symmetric] by blast


580 
qed


581 


582 
lemma finite_set_avoid:


583 
fixes a :: "'a::metric_space"


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


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


586 
case 1 thus ?case apply auto by ferrack


587 
next


588 
case (2 x F)


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


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


591 
moreover


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


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


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


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


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


597 
ultimately show ?case by blast


598 
qed


599 


600 
lemma islimpt_finite:


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


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


603 
unfolding islimpt_approachable


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


605 


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


607 
apply (rule iffI)


608 
defer


609 
apply (metis Un_upper1 Un_upper2 islimpt_subset)


610 
unfolding islimpt_def


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


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


613 
apply (auto simp add: open_Int)


614 
done


615 


616 
lemma discrete_imp_closed:


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


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


619 
shows "closed S"


620 
proof


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


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


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


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


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


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


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


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


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


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


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


632 
qed


633 


634 
subsection{* Interior of a Set *}


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


636 


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


638 
apply (simp add: expand_set_eq interior_def)


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


640 


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


642 


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


644 


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


646 
apply (simp add: interior_def)


647 
apply (subst open_subopen) by blast


648 


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


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


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


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


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


654 
by (metis equalityI interior_maximal interior_subset open_interior)


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


656 
apply (simp add: interior_def)


657 
by (metis open_contains_ball centre_in_ball open_ball subset_trans)


658 


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


660 
by (metis interior_maximal interior_subset subset_trans)


661 


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


663 
apply (rule equalityI, simp)


664 
apply (metis Int_lower1 Int_lower2 subset_interior)


665 
by (metis Int_mono interior_subset open_Int open_interior open_subset_interior)


666 


667 
lemma interior_limit_point [intro]:


668 
fixes x :: "'a::perfect_space"


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


670 
proof


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


672 
unfolding mem_interior subset_eq Ball_def mem_ball by blast


673 
{


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


675 
let ?m = "min d e"


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


677 
from perfect_choose_dist [OF mde2, of x]


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


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


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


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


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


683 
}


684 
then show ?thesis unfolding islimpt_approachable by blast


685 
qed


686 


687 
lemma interior_closed_Un_empty_interior:


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


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


690 
proof


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


692 
by (rule subset_interior, blast)


693 
next


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


695 
proof


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


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


698 
unfolding interior_def by fast


699 
show "x \<in> interior S"


700 
proof (rule ccontr)


701 
assume "x \<notin> interior S"


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


703 
unfolding interior_def expand_set_eq by fast


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


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


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


707 
show "False" unfolding interior_def by fast


708 
qed


709 
qed


710 
qed


711 


712 


713 
subsection{* Closure of a Set *}


714 


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


716 


717 
lemma closure_interior: "closure S = UNIV  interior (UNIV  S)"


718 
proof


719 
{ fix x


720 
have "x\<in>UNIV  interior (UNIV  S) \<longleftrightarrow> x \<in> closure S" (is "?lhs = ?rhs")


721 
proof


722 
let ?exT = "\<lambda> y. (\<exists>T. open T \<and> y \<in> T \<and> T \<subseteq> UNIV  S)"


723 
assume "?lhs"


724 
hence *:"\<not> ?exT x"


725 
unfolding interior_def


726 
by simp


727 
{ assume "\<not> ?rhs"


728 
hence False using *


729 
unfolding closure_def islimpt_def


730 
by blast


731 
}


732 
thus "?rhs"


733 
by blast


734 
next


735 
assume "?rhs" thus "?lhs"


736 
unfolding closure_def interior_def islimpt_def


737 
by blast


738 
qed


739 
}


740 
thus ?thesis


741 
by blast


742 
qed


743 


744 
lemma interior_closure: "interior S = UNIV  (closure (UNIV  S))"


745 
proof


746 
{ fix x


747 
have "x \<in> interior S \<longleftrightarrow> x \<in> UNIV  (closure (UNIV  S))"


748 
unfolding interior_def closure_def islimpt_def


749 
by blast (* FIXME: VERY slow! *)


750 
}


751 
thus ?thesis


752 
by blast


753 
qed


754 


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


756 
proof


757 
have "closed (UNIV  interior (UNIV S))" by blast


758 
thus ?thesis using closure_interior[of S] by simp


759 
qed


760 


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


762 
proof


763 
have "S \<subseteq> closure S"


764 
unfolding closure_def


765 
by blast


766 
moreover


767 
have "closed (closure S)"


768 
using closed_closure[of S]


769 
by assumption


770 
moreover


771 
{ fix t


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


773 
{ fix x


774 
assume "x islimpt S"


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


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


777 
by blast


778 
}


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


780 
unfolding closure_def


781 
using closed_limpt[of t]


782 
by auto


783 
}


784 
ultimately show ?thesis


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


786 
unfolding mem_def


787 
by simp


788 
qed


789 


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


791 
unfolding closure_hull


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


793 
by (metis mem_def subset_eq)


794 


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


796 
using closure_eq[of S]


797 
by simp


798 


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


800 
unfolding closure_hull


801 
using hull_hull[of closed S]


802 
by assumption


803 


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


805 
unfolding closure_hull


806 
using hull_subset[of S closed]


807 
by assumption


808 


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


810 
unfolding closure_hull


811 
using hull_mono[of S T closed]


812 
by assumption


813 


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


815 
using hull_minimal[of S T closed]


816 
unfolding closure_hull mem_def


817 
by simp


818 


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


820 
using hull_unique[of S T closed]


821 
unfolding closure_hull mem_def


822 
by simp


823 


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


825 
using closed_empty closure_closed[of "{}"]


826 
by simp


827 


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


829 
using closure_closed[of UNIV]


830 
by simp


831 


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


833 
using closure_empty closure_subset[of S]


834 
by blast


835 


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


837 
using closure_eq[of S] closure_subset[of S]


838 
by simp


839 


840 
lemma open_inter_closure_eq_empty:


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


842 
using open_subset_interior[of S "UNIV  T"]


843 
using interior_subset[of "UNIV  T"]


844 
unfolding closure_interior


845 
by auto


846 


847 
lemma open_inter_closure_subset:


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


849 
proof


850 
fix x


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


852 
{ assume *:"x islimpt T"


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


854 
proof (rule islimptI)


855 
fix A


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


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


858 
by (simp_all add: open_Int)


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


860 
by (rule islimptE)


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


862 
by simp_all


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


864 
qed


865 
}


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


867 
unfolding closure_def


868 
by blast


869 
qed


870 


871 
lemma closure_complement: "closure(UNIV  S) = UNIV  interior(S)"


872 
proof


873 
have "S = UNIV  (UNIV  S)"


874 
by auto


875 
thus ?thesis


876 
unfolding closure_interior


877 
by auto


878 
qed


879 


880 
lemma interior_complement: "interior(UNIV  S) = UNIV  closure(S)"


881 
unfolding closure_interior


882 
by blast


883 


884 
subsection{* Frontier (aka boundary) *}


885 


886 
definition "frontier S = closure S  interior S"


887 


888 
lemma frontier_closed: "closed(frontier S)"


889 
by (simp add: frontier_def closed_Diff)


890 


891 
lemma frontier_closures: "frontier S = (closure S) \<inter> (closure(UNIV  S))"


892 
by (auto simp add: frontier_def interior_closure)


893 


894 
lemma frontier_straddle:


895 
fixes a :: "'a::metric_space"


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


897 
proof


898 
assume "?lhs"


899 
{ fix e::real


900 
assume "e > 0"


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


902 
{ assume "a\<in>S"


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


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


905 
unfolding frontier_closures closure_def islimpt_def using `e>0`


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


907 
ultimately have ?rhse by auto


908 
}


909 
moreover


910 
{ assume "a\<notin>S"


911 
hence ?rhse using `?lhs`


912 
unfolding frontier_closures closure_def islimpt_def


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


914 
by (auto, erule_tac x = "ball a e" in allE, auto) (* FIXME: VERY slow! *)


915 
}


916 
ultimately have ?rhse by auto


917 
}


918 
thus ?rhs by auto


919 
next


920 
assume ?rhs


921 
moreover


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


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


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


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


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


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


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


929 
}


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


931 
moreover


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


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


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


935 
hence "\<exists>y\<in>UNIV  S. y \<in> T \<and> y \<noteq> a" using balle `a\<in>S` unfolding ball_def by (rule_tac x=x in bexI)auto


936 
}


937 
hence "a islimpt (UNIV  S) \<or> a\<notin>S" unfolding islimpt_def by auto


938 
ultimately show ?lhs unfolding frontier_closures using closure_def[of "UNIV  S"] by auto


939 
qed


940 


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


942 
by (metis frontier_def closure_closed Diff_subset)


943 


944 
lemma frontier_empty: "frontier {} = {}"


945 
by (simp add: frontier_def closure_empty)


946 


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


948 
proof


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


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


951 
hence "closed S" using closure_subset_eq by auto


952 
}


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


954 
qed


955 


956 
lemma frontier_complement: "frontier(UNIV  S) = frontier S"


957 
by (auto simp add: frontier_def closure_complement interior_complement)


958 


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


960 
using frontier_complement frontier_subset_eq[of "UNIV  S"]


961 
unfolding open_closed Compl_eq_Diff_UNIV by auto


962 


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


964 


965 
definition


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


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


968 


969 
definition


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


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


972 


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


974 


975 
lemma Rep_net_at_infinity:


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


977 
unfolding at_infinity_def


978 
apply (rule Abs_net_inverse')


979 
apply (rule image_nonempty, simp)


980 
apply (clarsimp, rename_tac r s)


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


982 
done


983 


984 
lemma within_UNIV: "net within UNIV = net"


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


986 


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


988 


989 
definition


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


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


992 


993 
lemma trivial_limit_within:


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


995 
proof


996 
assume "trivial_limit (at a within S)"


997 
thus "\<not> a islimpt S"


998 
unfolding trivial_limit_def


999 
unfolding Rep_net_within Rep_net_at


1000 
unfolding islimpt_def


1001 
apply (clarsimp simp add: expand_set_eq)


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


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


1004 
done


1005 
next


1006 
assume "\<not> a islimpt S"


1007 
thus "trivial_limit (at a within S)"


1008 
unfolding trivial_limit_def


1009 
unfolding Rep_net_within Rep_net_at


1010 
unfolding islimpt_def


1011 
apply (clarsimp simp add: image_image)


1012 
apply (rule_tac x=T in image_eqI)


1013 
apply (auto simp add: expand_set_eq)


1014 
done


1015 
qed


1016 


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


1018 
using trivial_limit_within [of a UNIV]


1019 
by (simp add: within_UNIV)


1020 


1021 
lemma trivial_limit_at:


1022 
fixes a :: "'a::perfect_space"


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


1024 
by (simp add: trivial_limit_at_iff)


1025 


1026 
lemma trivial_limit_at_infinity:


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


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


1029 
unfolding trivial_limit_def Rep_net_at_infinity


1030 
apply (clarsimp simp add: expand_set_eq)


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


1032 
apply (simp add: norm_sgn)


1033 
done


1034 


1035 
lemma trivial_limit_sequentially: "\<not> trivial_limit sequentially"


1036 
by (auto simp add: trivial_limit_def Rep_net_sequentially)


1037 


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


1039 


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


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


1042 
unfolding eventually_at dist_nz by auto


1043 


1044 
lemma eventually_at_infinity:


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


1046 
unfolding eventually_def Rep_net_at_infinity by auto


1047 


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


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


1050 
unfolding eventually_within eventually_at dist_nz by auto


1051 


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


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


1054 
unfolding eventually_within


1055 
apply safe


1056 
apply (rule_tac x="d/2" in exI, simp)


1057 
apply (rule_tac x="d" in exI, simp)


1058 
done


1059 


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


1061 
unfolding eventually_def trivial_limit_def


1062 
using Rep_net_nonempty [of net] by auto


1063 


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


1065 
unfolding eventually_def trivial_limit_def


1066 
using Rep_net_nonempty [of net] by auto


1067 


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


1069 
unfolding trivial_limit_def eventually_def by auto


1070 


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


1072 
unfolding trivial_limit_def eventually_def by auto


1073 


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


1075 
apply (safe elim!: trivial_limit_eventually)


1076 
apply (simp add: eventually_False [symmetric])


1077 
done


1078 


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


1080 


1081 
lemma eventually_conjI:


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


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


1084 
by (rule eventually_conj)


1085 


1086 
lemma eventually_rev_mono:


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


1088 
using eventually_mono [of P Q] by fast


1089 


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


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


1092 


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


1094 
by (auto simp add: eventually_False)


1095 


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


1097 
by (simp add: eventually_False)


1098 


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


1100 


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


1102 
definition


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


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


1105 


1106 
lemma Lim:


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


1108 
trivial_limit net \<or>


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


1110 
unfolding tendsto_iff trivial_limit_eq by auto


1111 


1112 


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


1114 


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


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


1117 
by (auto simp add: tendsto_iff eventually_within_le)


1118 


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


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


1121 
by (auto simp add: tendsto_iff eventually_within)


1122 


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


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


1125 
by (auto simp add: tendsto_iff eventually_at)


1126 


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


1128 
unfolding Lim_at LIM_def by (simp only: zero_less_dist_iff)


1129 


1130 
lemma Lim_at_infinity:


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


1132 
by (auto simp add: tendsto_iff eventually_at_infinity)


1133 


1134 
lemma Lim_sequentially:


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


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


1137 
by (auto simp add: tendsto_iff eventually_sequentially)


1138 


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


1140 
unfolding Lim_sequentially LIMSEQ_def ..


1141 


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


1143 
by (rule topological_tendstoI, auto elim: eventually_rev_mono)


1144 


1145 
text{* The expected monotonicity property. *}


1146 


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


1148 
unfolding tendsto_def Limits.eventually_within by simp


1149 


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


1151 
unfolding tendsto_def Limits.eventually_within


1152 
by (auto elim!: eventually_elim1)


1153 


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


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


1156 
using assms unfolding tendsto_def Limits.eventually_within


1157 
apply clarify


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


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


1160 
apply (auto elim: eventually_elim2)


1161 
done


1162 


1163 
lemma Lim_Un_univ:


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


1165 
==> (f > l) net"


1166 
by (metis Lim_Un within_UNIV)


1167 


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


1169 


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


1171 
(* FIXME: rename *)


1172 
unfolding tendsto_def Limits.eventually_within


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


1174 
by (auto elim!: eventually_elim1)


1175 


1176 
lemma Lim_within_open:


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


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


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


1180 
proof


1181 
assume ?lhs


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


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


1184 
by (rule topological_tendstoD)


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


1186 
unfolding Limits.eventually_within .


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


1188 
unfolding eventually_at_topological by fast


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


1190 
using assms by auto


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


1192 
by fast


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


1194 
unfolding eventually_at_topological .


1195 
}


1196 
thus ?rhs by (rule topological_tendstoI)


1197 
next


1198 
assume ?rhs


1199 
thus ?lhs by (rule Lim_at_within)


1200 
qed


1201 


1202 
text{* Another limit point characterization. *}


1203 


1204 
lemma islimpt_sequential:


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


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


1207 
(is "?lhs = ?rhs")


1208 
proof


1209 
assume ?lhs


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


1211 
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


1212 
{ fix n::nat


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


1214 
}


1215 
moreover


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


1217 
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


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


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


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


1221 
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


1222 
}


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


1224 
unfolding Lim_sequentially using f by auto


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


1226 
next


1227 
assume ?rhs


1228 
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


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


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


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


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


1233 
}


1234 
thus ?lhs unfolding islimpt_approachable by auto


1235 
qed


1236 


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


1238 


1239 
lemma Lim_linear:


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


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


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


1243 
by (rule bounded_linear.tendsto)


1244 


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


1246 
unfolding tendsto_def Limits.eventually_at_topological by fast


1247 


1248 
lemma Lim_const: "((\<lambda>x. a) > a) net"


1249 
by (rule tendsto_const)


1250 


1251 
lemma Lim_cmul:


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


1253 
shows "(f > l) net ==> ((\<lambda>x. c *\<^sub>R f x) > c *\<^sub>R l) net"


1254 
by (intro tendsto_intros)


1255 


1256 
lemma Lim_neg:


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


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


1259 
by (rule tendsto_minus)


1260 


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


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


1263 
by (rule tendsto_add)


1264 


1265 
lemma Lim_sub:


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


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


1268 
by (rule tendsto_diff)


1269 


1270 
lemma Lim_null:


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


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


1273 


1274 
lemma Lim_null_norm:


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


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


1277 
by (simp add: Lim dist_norm)


1278 


1279 
lemma Lim_null_comparison:


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


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


1282 
shows "(f > 0) net"


1283 
proof(simp add: tendsto_iff, rule+)


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


1285 
{ fix x


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


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


1288 
}


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


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


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


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


1293 
qed


1294 


1295 
lemma Lim_component:


1296 
fixes f :: "'a \<Rightarrow> 'b::metric_space ^ 'n::finite"


1297 
shows "(f > l) net \<Longrightarrow> ((\<lambda>a. f a $i) > l$i) net"


1298 
unfolding tendsto_iff


1299 
apply (clarify)


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


1301 
apply (erule eventually_elim1)


1302 
apply (erule le_less_trans [OF dist_nth_le])


1303 
done


1304 


1305 
lemma Lim_transform_bound:


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


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


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


1309 
shows "(f > 0) net"


1310 
proof (rule tendstoI)


1311 
fix e::real assume "e>0"


1312 
{ fix x


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


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


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


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


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


1318 
using assms `e>0` unfolding tendsto_iff by blast


1319 
qed


1320 


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


1322 


1323 
lemma Lim_in_closed_set:


1324 
assumes "closed S" "ev 