Topology_Euclidean_Space.thy: organize section headings
authorhuffman
Mon Aug 15 10:49:48 2011 -0700 (2011-08-15)
changeset 44210eba74571833b
parent 44209 00d3147dd639
child 44211 bd7c586b902e
Topology_Euclidean_Space.thy: organize section headings
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Aug 15 09:08:17 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Aug 15 10:49:48 2011 -0700
     1.3 @@ -20,7 +20,7 @@
     1.4    apply(subst(2) euclidean_dist_l2) apply(cases "i<DIM('a)")
     1.5    apply(rule member_le_setL2) by auto
     1.6  
     1.7 -subsection{* General notion of a topology *}
     1.8 +subsection {* General notion of a topologies as values *}
     1.9  
    1.10  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))"
    1.11  typedef (open) 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
    1.12 @@ -51,7 +51,7 @@
    1.13  
    1.14  definition "topspace T =  \<Union>{S. openin T S}"
    1.15  
    1.16 -subsection{* Main properties of open sets *}
    1.17 +subsubsection {* Main properties of open sets *}
    1.18  
    1.19  lemma openin_clauses:
    1.20    fixes U :: "'a topology"
    1.21 @@ -87,7 +87,7 @@
    1.22    finally show "openin U S" .
    1.23  qed
    1.24  
    1.25 -subsection{* Closed sets *}
    1.26 +subsubsection {* Closed sets *}
    1.27  
    1.28  definition "closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U - S)"
    1.29  
    1.30 @@ -128,10 +128,7 @@
    1.31    then show ?thesis using oS cT by (auto simp add: openin_closedin_eq)
    1.32  qed
    1.33  
    1.34 -subsection{* Subspace topology. *}
    1.35 -
    1.36 -term "{f x |x. P x}"
    1.37 -term "{y. \<exists>x. y = f x \<and> P x}"
    1.38 +subsubsection {* Subspace topology *}
    1.39  
    1.40  definition "subtopology U V = topology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
    1.41  
    1.42 @@ -197,14 +194,13 @@
    1.43    then show ?thesis unfolding topology_eq openin_subtopology by blast
    1.44  qed
    1.45  
    1.46 -
    1.47  lemma subtopology_topspace[simp]: "subtopology U (topspace U) = U"
    1.48    by (simp add: subtopology_superset)
    1.49  
    1.50  lemma subtopology_UNIV[simp]: "subtopology U UNIV = U"
    1.51    by (simp add: subtopology_superset)
    1.52  
    1.53 -subsection{* The universal Euclidean versions are what we use most of the time *}
    1.54 +subsubsection {* The standard Euclidean topology *}
    1.55  
    1.56  definition
    1.57    euclidean :: "'a::topological_space topology" where
    1.58 @@ -231,7 +227,83 @@
    1.59  lemma open_subopen: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S)"
    1.60    by (simp add: open_openin openin_subopen[symmetric])
    1.61  
    1.62 -subsection{* Open and closed balls. *}
    1.63 +text {* Basic "localization" results are handy for connectedness. *}
    1.64 +
    1.65 +lemma openin_open: "openin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. open T \<and> (S = U \<inter> T))"
    1.66 +  by (auto simp add: openin_subtopology open_openin[symmetric])
    1.67 +
    1.68 +lemma openin_open_Int[intro]: "open S \<Longrightarrow> openin (subtopology euclidean U) (U \<inter> S)"
    1.69 +  by (auto simp add: openin_open)
    1.70 +
    1.71 +lemma open_openin_trans[trans]:
    1.72 + "open S \<Longrightarrow> open T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> openin (subtopology euclidean S) T"
    1.73 +  by (metis Int_absorb1  openin_open_Int)
    1.74 +
    1.75 +lemma open_subset:  "S \<subseteq> T \<Longrightarrow> open S \<Longrightarrow> openin (subtopology euclidean T) S"
    1.76 +  by (auto simp add: openin_open)
    1.77 +
    1.78 +lemma closedin_closed: "closedin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. closed T \<and> S = U \<inter> T)"
    1.79 +  by (simp add: closedin_subtopology closed_closedin Int_ac)
    1.80 +
    1.81 +lemma closedin_closed_Int: "closed S ==> closedin (subtopology euclidean U) (U \<inter> S)"
    1.82 +  by (metis closedin_closed)
    1.83 +
    1.84 +lemma closed_closedin_trans: "closed S \<Longrightarrow> closed T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> closedin (subtopology euclidean S) T"
    1.85 +  apply (subgoal_tac "S \<inter> T = T" )
    1.86 +  apply auto
    1.87 +  apply (frule closedin_closed_Int[of T S])
    1.88 +  by simp
    1.89 +
    1.90 +lemma closed_subset: "S \<subseteq> T \<Longrightarrow> closed S \<Longrightarrow> closedin (subtopology euclidean T) S"
    1.91 +  by (auto simp add: closedin_closed)
    1.92 +
    1.93 +lemma openin_euclidean_subtopology_iff:
    1.94 +  fixes S U :: "'a::metric_space set"
    1.95 +  shows "openin (subtopology euclidean U) S
    1.96 +  \<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")
    1.97 +proof
    1.98 +  assume ?lhs thus ?rhs unfolding openin_open open_dist by blast
    1.99 +next
   1.100 +  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}"
   1.101 +  have 1: "\<forall>x\<in>T. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> T"
   1.102 +    unfolding T_def
   1.103 +    apply clarsimp
   1.104 +    apply (rule_tac x="d - dist x a" in exI)
   1.105 +    apply (clarsimp simp add: less_diff_eq)
   1.106 +    apply (erule rev_bexI)
   1.107 +    apply (rule_tac x=d in exI, clarify)
   1.108 +    apply (erule le_less_trans [OF dist_triangle])
   1.109 +    done
   1.110 +  assume ?rhs hence 2: "S = U \<inter> T"
   1.111 +    unfolding T_def
   1.112 +    apply auto
   1.113 +    apply (drule (1) bspec, erule rev_bexI)
   1.114 +    apply auto
   1.115 +    done
   1.116 +  from 1 2 show ?lhs
   1.117 +    unfolding openin_open open_dist by fast
   1.118 +qed
   1.119 +
   1.120 +text {* These "transitivity" results are handy too *}
   1.121 +
   1.122 +lemma openin_trans[trans]: "openin (subtopology euclidean T) S \<Longrightarrow> openin (subtopology euclidean U) T
   1.123 +  \<Longrightarrow> openin (subtopology euclidean U) S"
   1.124 +  unfolding open_openin openin_open by blast
   1.125 +
   1.126 +lemma openin_open_trans: "openin (subtopology euclidean T) S \<Longrightarrow> open T \<Longrightarrow> open S"
   1.127 +  by (auto simp add: openin_open intro: openin_trans)
   1.128 +
   1.129 +lemma closedin_trans[trans]:
   1.130 + "closedin (subtopology euclidean T) S \<Longrightarrow>
   1.131 +           closedin (subtopology euclidean U) T
   1.132 +           ==> closedin (subtopology euclidean U) S"
   1.133 +  by (auto simp add: closedin_closed closed_closedin closed_Inter Int_assoc)
   1.134 +
   1.135 +lemma closedin_closed_trans: "closedin (subtopology euclidean T) S \<Longrightarrow> closed T \<Longrightarrow> closed S"
   1.136 +  by (auto simp add: closedin_closed intro: closedin_trans)
   1.137 +
   1.138 +
   1.139 +subsection {* Open and closed balls *}
   1.140  
   1.141  definition
   1.142    ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" where
   1.143 @@ -301,82 +373,6 @@
   1.144  
   1.145  lemma ball_empty[intro]: "e \<le> 0 ==> ball x e = {}" by simp
   1.146  
   1.147 -subsection{* Basic "localization" results are handy for connectedness. *}
   1.148 -
   1.149 -lemma openin_open: "openin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. open T \<and> (S = U \<inter> T))"
   1.150 -  by (auto simp add: openin_subtopology open_openin[symmetric])
   1.151 -
   1.152 -lemma openin_open_Int[intro]: "open S \<Longrightarrow> openin (subtopology euclidean U) (U \<inter> S)"
   1.153 -  by (auto simp add: openin_open)
   1.154 -
   1.155 -lemma open_openin_trans[trans]:
   1.156 - "open S \<Longrightarrow> open T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> openin (subtopology euclidean S) T"
   1.157 -  by (metis Int_absorb1  openin_open_Int)
   1.158 -
   1.159 -lemma open_subset:  "S \<subseteq> T \<Longrightarrow> open S \<Longrightarrow> openin (subtopology euclidean T) S"
   1.160 -  by (auto simp add: openin_open)
   1.161 -
   1.162 -lemma closedin_closed: "closedin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. closed T \<and> S = U \<inter> T)"
   1.163 -  by (simp add: closedin_subtopology closed_closedin Int_ac)
   1.164 -
   1.165 -lemma closedin_closed_Int: "closed S ==> closedin (subtopology euclidean U) (U \<inter> S)"
   1.166 -  by (metis closedin_closed)
   1.167 -
   1.168 -lemma closed_closedin_trans: "closed S \<Longrightarrow> closed T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> closedin (subtopology euclidean S) T"
   1.169 -  apply (subgoal_tac "S \<inter> T = T" )
   1.170 -  apply auto
   1.171 -  apply (frule closedin_closed_Int[of T S])
   1.172 -  by simp
   1.173 -
   1.174 -lemma closed_subset: "S \<subseteq> T \<Longrightarrow> closed S \<Longrightarrow> closedin (subtopology euclidean T) S"
   1.175 -  by (auto simp add: closedin_closed)
   1.176 -
   1.177 -lemma openin_euclidean_subtopology_iff:
   1.178 -  fixes S U :: "'a::metric_space set"
   1.179 -  shows "openin (subtopology euclidean U) S
   1.180 -  \<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")
   1.181 -proof-
   1.182 -  {assume ?lhs hence ?rhs unfolding openin_subtopology open_openin[symmetric]
   1.183 -      by (simp add: open_dist) blast}
   1.184 -  moreover
   1.185 -  {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"
   1.186 -    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)"
   1.187 -      by metis
   1.188 -    let ?T = "\<Union>{B. \<exists>x\<in>S. B = ball x (d x)}"
   1.189 -    have oT: "open ?T" by auto
   1.190 -    { fix x assume "x\<in>S"
   1.191 -      hence "x \<in> \<Union>{B. \<exists>x\<in>S. B = ball x (d x)}"
   1.192 -        apply simp apply(rule_tac x="ball x(d x)" in exI) apply auto
   1.193 -        by (rule d [THEN conjunct1])
   1.194 -      hence "x\<in> ?T \<inter> U" using SU and `x\<in>S` by auto  }
   1.195 -    moreover
   1.196 -    { fix y assume "y\<in>?T"
   1.197 -      then obtain B where "y\<in>B" "B\<in>{B. \<exists>x\<in>S. B = ball x (d x)}" by auto
   1.198 -      then obtain x where "x\<in>S" and x:"y \<in> ball x (d x)" by auto
   1.199 -      assume "y\<in>U"
   1.200 -      hence "y\<in>S" using d[OF `x\<in>S`] and x by(auto simp add: dist_commute) }
   1.201 -    ultimately have "S = ?T \<inter> U" by blast
   1.202 -    with oT have ?lhs unfolding openin_subtopology open_openin[symmetric] by blast}
   1.203 -  ultimately show ?thesis by blast
   1.204 -qed
   1.205 -
   1.206 -text{* These "transitivity" results are handy too. *}
   1.207 -
   1.208 -lemma openin_trans[trans]: "openin (subtopology euclidean T) S \<Longrightarrow> openin (subtopology euclidean U) T
   1.209 -  \<Longrightarrow> openin (subtopology euclidean U) S"
   1.210 -  unfolding open_openin openin_open by blast
   1.211 -
   1.212 -lemma openin_open_trans: "openin (subtopology euclidean T) S \<Longrightarrow> open T \<Longrightarrow> open S"
   1.213 -  by (auto simp add: openin_open intro: openin_trans)
   1.214 -
   1.215 -lemma closedin_trans[trans]:
   1.216 - "closedin (subtopology euclidean T) S \<Longrightarrow>
   1.217 -           closedin (subtopology euclidean U) T
   1.218 -           ==> closedin (subtopology euclidean U) S"
   1.219 -  by (auto simp add: closedin_closed closed_closedin closed_Inter Int_assoc)
   1.220 -
   1.221 -lemma closedin_closed_trans: "closedin (subtopology euclidean T) S \<Longrightarrow> closed T \<Longrightarrow> closed S"
   1.222 -  by (auto simp add: closedin_closed intro: closedin_trans)
   1.223  
   1.224  subsection{* Connectedness *}
   1.225  
   1.226 @@ -430,6 +426,7 @@
   1.227  lemma connected_empty[simp, intro]: "connected {}"
   1.228    by (simp add: connected_def)
   1.229  
   1.230 +
   1.231  subsection{* Limit points *}
   1.232  
   1.233  definition (in topological_space)
   1.234 @@ -468,6 +465,8 @@
   1.235    using approachable_lt_le[where f="\<lambda>x'. dist x' x" and P="\<lambda>x'. \<not> (x'\<in>S \<and> x'\<noteq>x)"]
   1.236    by metis 
   1.237  
   1.238 +text {* A perfect space has no isolated points. *}
   1.239 +
   1.240  class perfect_space = topological_space +
   1.241    assumes islimpt_UNIV [simp, intro]: "x islimpt UNIV"
   1.242  
   1.243 @@ -553,7 +552,9 @@
   1.244    then show ?thesis by (metis islimpt_approachable closed_limpt [where 'a='a])
   1.245  qed
   1.246  
   1.247 -subsection{* Interior of a Set *}
   1.248 +
   1.249 +subsection {* Interior of a Set *}
   1.250 +
   1.251  definition "interior S = {x. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S}"
   1.252  
   1.253  lemma interior_eq: "interior S = S \<longleftrightarrow> open S"
   1.254 @@ -622,7 +623,7 @@
   1.255  qed
   1.256  
   1.257  
   1.258 -subsection{* Closure of a Set *}
   1.259 +subsection {* Closure of a Set *}
   1.260  
   1.261  definition "closure S = S \<union> {x | x. x islimpt S}"
   1.262  
   1.263 @@ -792,7 +793,8 @@
   1.264    unfolding closure_interior
   1.265    by blast
   1.266  
   1.267 -subsection{* Frontier (aka boundary) *}
   1.268 +
   1.269 +subsection {* Frontier (aka boundary) *}
   1.270  
   1.271  definition "frontier S = closure S - interior S"
   1.272  
   1.273 @@ -871,10 +873,9 @@
   1.274    using frontier_complement frontier_subset_eq[of "- S"]
   1.275    unfolding open_closed by auto
   1.276  
   1.277 +
   1.278  subsection {* Filters and the ``eventually true'' quantifier *}
   1.279  
   1.280 -text {* Common filters and The "within" modifier for filters. *}
   1.281 -
   1.282  definition
   1.283    at_infinity :: "'a::real_normed_vector filter" where
   1.284    "at_infinity = Abs_filter (\<lambda>P. \<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x)"
   1.285 @@ -968,7 +969,6 @@
   1.286  lemma eventually_False: "eventually (\<lambda>x. False) net \<longleftrightarrow> trivial_limit net"
   1.287    unfolding trivial_limit_def ..
   1.288  
   1.289 -
   1.290  lemma trivial_limit_eq: "trivial_limit net \<longleftrightarrow> (\<forall>P. eventually P net)"
   1.291    apply (safe elim!: trivial_limit_eventually)
   1.292    apply (simp add: eventually_False [symmetric])
   1.293 @@ -979,21 +979,22 @@
   1.294  lemma eventually_conjI:
   1.295    "\<lbrakk>eventually (\<lambda>x. P x) net; eventually (\<lambda>x. Q x) net\<rbrakk>
   1.296      \<Longrightarrow> eventually (\<lambda>x. P x \<and> Q x) net"
   1.297 -by (rule eventually_conj)
   1.298 +by (rule eventually_conj) (* FIXME: delete *)
   1.299  
   1.300  lemma eventually_rev_mono:
   1.301    "eventually P net \<Longrightarrow> (\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually Q net"
   1.302  using eventually_mono [of P Q] by fast
   1.303  
   1.304  lemma eventually_and: " eventually (\<lambda>x. P x \<and> Q x) net \<longleftrightarrow> eventually P net \<and> eventually Q net"
   1.305 -  by (auto intro!: eventually_conjI elim: eventually_rev_mono)
   1.306 +  by (rule eventually_conj_iff) (* FIXME: delete *)
   1.307  
   1.308  lemma eventually_false: "eventually (\<lambda>x. False) net \<longleftrightarrow> trivial_limit net"
   1.309 -  by (auto simp add: eventually_False)
   1.310 +  by (rule eventually_False) (* FIXME: delete *)
   1.311  
   1.312  lemma not_eventually: "(\<forall>x. \<not> P x ) \<Longrightarrow> ~(trivial_limit net) ==> ~(eventually (\<lambda>x. P x) net)"
   1.313    by (simp add: eventually_False)
   1.314  
   1.315 +
   1.316  subsection {* Limits *}
   1.317  
   1.318  text{* Notation Lim to avoid collition with lim defined in analysis *}
   1.319 @@ -1007,7 +1008,6 @@
   1.320          (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
   1.321    unfolding tendsto_iff trivial_limit_eq by auto
   1.322  
   1.323 -
   1.324  text{* Show that they yield usual definitions in the various cases. *}
   1.325  
   1.326  lemma Lim_within_le: "(f ---> l)(at a within S) \<longleftrightarrow>
   1.327 @@ -1032,7 +1032,7 @@
   1.328  lemma Lim_sequentially:
   1.329   "(S ---> l) sequentially \<longleftrightarrow>
   1.330            (\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (S n) l < e)"
   1.331 -  by (auto simp add: tendsto_iff eventually_sequentially)
   1.332 +  by (rule LIMSEQ_def) (* FIXME: redundant *)
   1.333  
   1.334  lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f ---> l) net"
   1.335    by (rule topological_tendstoI, auto elim: eventually_rev_mono)
   1.336 @@ -1068,31 +1068,41 @@
   1.337    apply (clarify, drule spec, drule (1) mp, drule (1) mp)
   1.338    by (auto elim!: eventually_elim1)
   1.339  
   1.340 +lemma eventually_within_interior:
   1.341 +  assumes "x \<in> interior S"
   1.342 +  shows "eventually P (at x within S) \<longleftrightarrow> eventually P (at x)" (is "?lhs = ?rhs")
   1.343 +proof-
   1.344 +  from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S"
   1.345 +    unfolding interior_def by fast
   1.346 +  { assume "?lhs"
   1.347 +    then obtain A where "open A" "x \<in> A" "\<forall>y\<in>A. y \<noteq> x \<longrightarrow> y \<in> S \<longrightarrow> P y"
   1.348 +      unfolding Limits.eventually_within Limits.eventually_at_topological
   1.349 +      by auto
   1.350 +    with T have "open (A \<inter> T)" "x \<in> A \<inter> T" "\<forall>y\<in>(A \<inter> T). y \<noteq> x \<longrightarrow> P y"
   1.351 +      by auto
   1.352 +    then have "?rhs"
   1.353 +      unfolding Limits.eventually_at_topological by auto
   1.354 +  } moreover
   1.355 +  { assume "?rhs" hence "?lhs"
   1.356 +      unfolding Limits.eventually_within
   1.357 +      by (auto elim: eventually_elim1)
   1.358 +  } ultimately
   1.359 +  show "?thesis" ..
   1.360 +qed
   1.361 +
   1.362 +lemma at_within_interior:
   1.363 +  "x \<in> interior S \<Longrightarrow> at x within S = at x"
   1.364 +  by (simp add: filter_eq_iff eventually_within_interior)
   1.365 +
   1.366 +lemma at_within_open:
   1.367 +  "\<lbrakk>x \<in> S; open S\<rbrakk> \<Longrightarrow> at x within S = at x"
   1.368 +  by (simp only: at_within_interior interior_open)
   1.369 +
   1.370  lemma Lim_within_open:
   1.371    fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
   1.372    assumes"a \<in> S" "open S"
   1.373 -  shows "(f ---> l)(at a within S) \<longleftrightarrow> (f ---> l)(at a)" (is "?lhs \<longleftrightarrow> ?rhs")
   1.374 -proof
   1.375 -  assume ?lhs
   1.376 -  { fix A assume "open A" "l \<in> A"
   1.377 -    with `?lhs` have "eventually (\<lambda>x. f x \<in> A) (at a within S)"
   1.378 -      by (rule topological_tendstoD)
   1.379 -    hence "eventually (\<lambda>x. x \<in> S \<longrightarrow> f x \<in> A) (at a)"
   1.380 -      unfolding Limits.eventually_within .
   1.381 -    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"
   1.382 -      unfolding eventually_at_topological by fast
   1.383 -    hence "open (T \<inter> S)" "a \<in> T \<inter> S" "\<forall>x\<in>(T \<inter> S). x \<noteq> a \<longrightarrow> f x \<in> A"
   1.384 -      using assms by auto
   1.385 -    hence "\<exists>T. open T \<and> a \<in> T \<and> (\<forall>x\<in>T. x \<noteq> a \<longrightarrow> f x \<in> A)"
   1.386 -      by fast
   1.387 -    hence "eventually (\<lambda>x. f x \<in> A) (at a)"
   1.388 -      unfolding eventually_at_topological .
   1.389 -  }
   1.390 -  thus ?rhs by (rule topological_tendstoI)
   1.391 -next
   1.392 -  assume ?rhs
   1.393 -  thus ?lhs by (rule Lim_at_within)
   1.394 -qed
   1.395 +  shows "(f ---> l)(at a within S) \<longleftrightarrow> (f ---> l)(at a)"
   1.396 +  using assms by (simp only: at_within_open)
   1.397  
   1.398  lemma Lim_within_LIMSEQ:
   1.399    fixes a :: real and L :: "'a::metric_space"
   1.400 @@ -1432,6 +1442,16 @@
   1.401    using netlimit_within[of a UNIV]
   1.402    by (simp add: trivial_limit_at within_UNIV)
   1.403  
   1.404 +lemma lim_within_interior:
   1.405 +  "x \<in> interior S \<Longrightarrow> (f ---> l) (at x within S) \<longleftrightarrow> (f ---> l) (at x)"
   1.406 +  by (simp add: at_within_interior)
   1.407 +
   1.408 +lemma netlimit_within_interior:
   1.409 +  fixes x :: "'a::{t2_space,perfect_space}"
   1.410 +  assumes "x \<in> interior S"
   1.411 +  shows "netlimit (at x within S) = x"
   1.412 +using assms by (simp add: at_within_interior netlimit_at)
   1.413 +
   1.414  text{* Transformation of limit. *}
   1.415  
   1.416  lemma Lim_transform:
   1.417 @@ -1602,7 +1622,7 @@
   1.418    thus ?thesis unfolding Lim_sequentially dist_norm by simp
   1.419  qed
   1.420  
   1.421 -subsection {* More properties of closed balls. *}
   1.422 +subsection {* More properties of closed balls *}
   1.423  
   1.424  lemma closed_cball: "closed (cball x e)"
   1.425  unfolding cball_def closed_def
   1.426 @@ -1839,45 +1859,8 @@
   1.427    shows "e = 0 ==> cball x e = {x}"
   1.428    by (auto simp add: set_eq_iff)
   1.429  
   1.430 -text{* For points in the interior, localization of limits makes no difference.   *}
   1.431 -
   1.432 -lemma eventually_within_interior:
   1.433 -  assumes "x \<in> interior S"
   1.434 -  shows "eventually P (at x within S) \<longleftrightarrow> eventually P (at x)" (is "?lhs = ?rhs")
   1.435 -proof-
   1.436 -  from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S"
   1.437 -    unfolding interior_def by fast
   1.438 -  { assume "?lhs"
   1.439 -    then obtain A where "open A" "x \<in> A" "\<forall>y\<in>A. y \<noteq> x \<longrightarrow> y \<in> S \<longrightarrow> P y"
   1.440 -      unfolding Limits.eventually_within Limits.eventually_at_topological
   1.441 -      by auto
   1.442 -    with T have "open (A \<inter> T)" "x \<in> A \<inter> T" "\<forall>y\<in>(A \<inter> T). y \<noteq> x \<longrightarrow> P y"
   1.443 -      by auto
   1.444 -    then have "?rhs"
   1.445 -      unfolding Limits.eventually_at_topological by auto
   1.446 -  } moreover
   1.447 -  { assume "?rhs" hence "?lhs"
   1.448 -      unfolding Limits.eventually_within
   1.449 -      by (auto elim: eventually_elim1)
   1.450 -  } ultimately
   1.451 -  show "?thesis" ..
   1.452 -qed
   1.453 -
   1.454 -lemma at_within_interior:
   1.455 -  "x \<in> interior S \<Longrightarrow> at x within S = at x"
   1.456 -  by (simp add: filter_eq_iff eventually_within_interior)
   1.457 -
   1.458 -lemma lim_within_interior:
   1.459 -  "x \<in> interior S \<Longrightarrow> (f ---> l) (at x within S) \<longleftrightarrow> (f ---> l) (at x)"
   1.460 -  by (simp add: at_within_interior)
   1.461 -
   1.462 -lemma netlimit_within_interior:
   1.463 -  fixes x :: "'a::{t2_space,perfect_space}"
   1.464 -  assumes "x \<in> interior S"
   1.465 -  shows "netlimit (at x within S) = x"
   1.466 -using assms by (simp add: at_within_interior netlimit_at)
   1.467 -
   1.468 -subsection{* Boundedness. *}
   1.469 +
   1.470 +subsection {* Boundedness *}
   1.471  
   1.472    (* FIXME: This has to be unified with BSEQ!! *)
   1.473  definition (in metric_space)
   1.474 @@ -2076,7 +2059,6 @@
   1.475    shows "finite S ==> Inf(insert x S) = (if S = {} then x else min x (Inf S))"
   1.476    by (rule Inf_insert, rule finite_imp_bounded, simp)
   1.477  
   1.478 -
   1.479  (* TODO: Move this to RComplete.thy -- would need to include Glb into RComplete *)
   1.480  lemma real_isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::real)"
   1.481    apply (frule isGlb_isLb)
   1.482 @@ -2084,6 +2066,7 @@
   1.483    apply (blast intro!: order_antisym dest!: isGlb_le_isLb)
   1.484    done
   1.485  
   1.486 +
   1.487  subsection {* Equivalent versions of compactness *}
   1.488  
   1.489  subsubsection{* Sequential compactness *}
   1.490 @@ -2927,7 +2910,7 @@
   1.491    thus ?thesis unfolding closed_sequential_limits by fast
   1.492  qed
   1.493  
   1.494 -text{* Hence express everything as an equivalence.   *}
   1.495 +text {* Hence express everything as an equivalence. *}
   1.496  
   1.497  lemma compact_eq_heine_borel:
   1.498    fixes s :: "'a::metric_space set"
   1.499 @@ -3116,7 +3099,8 @@
   1.500    thus False using f'(3) unfolding subset_eq and Union_iff by blast
   1.501  qed
   1.502  
   1.503 -subsection{* Bounded closed nest property (proof does not use Heine-Borel).            *}
   1.504 +
   1.505 +subsection {* Bounded closed nest property (proof does not use Heine-Borel) *}
   1.506  
   1.507  lemma bounded_closed_nest:
   1.508    assumes "\<forall>n. closed(s n)" "\<forall>n. (s n \<noteq> {})"
   1.509 @@ -3146,7 +3130,7 @@
   1.510    thus ?thesis by auto
   1.511  qed
   1.512  
   1.513 -text{* Decreasing case does not even need compactness, just completeness.        *}
   1.514 +text {* Decreasing case does not even need compactness, just completeness. *}
   1.515  
   1.516  lemma decreasing_closed_nest:
   1.517    assumes "\<forall>n. closed(s n)"
   1.518 @@ -3179,7 +3163,7 @@
   1.519    then show ?thesis by auto
   1.520  qed
   1.521  
   1.522 -text{* Strengthen it to the intersection actually being a singleton.             *}
   1.523 +text {* Strengthen it to the intersection actually being a singleton. *}
   1.524  
   1.525  lemma decreasing_closed_nest_sing:
   1.526    fixes s :: "nat \<Rightarrow> 'a::heine_borel set"
   1.527 @@ -3250,6 +3234,7 @@
   1.528    ultimately show ?thesis by auto
   1.529  qed
   1.530  
   1.531 +
   1.532  subsection {* Continuity *}
   1.533  
   1.534  text {* Define continuity over a net to take in restrictions of the set. *}
   1.535 @@ -3423,7 +3408,7 @@
   1.536    unfolding continuous_on_def tendsto_def Limits.eventually_within
   1.537    by simp
   1.538  
   1.539 -text{* Characterization of various kinds of continuity in terms of sequences.  *}
   1.540 +text {* Characterization of various kinds of continuity in terms of sequences. *}
   1.541  
   1.542  (* \<longrightarrow> could be generalized, but \<longleftarrow> requires metric space *)
   1.543  lemma continuous_within_sequentially:
   1.544 @@ -3798,7 +3783,7 @@
   1.545    thus ?lhs unfolding continuous_on_open by auto
   1.546  qed
   1.547  
   1.548 -text{* Half-global and completely global cases.                                  *}
   1.549 +text {* Half-global and completely global cases. *}
   1.550  
   1.551  lemma continuous_open_in_preimage:
   1.552    assumes "continuous_on s f"  "open t"
   1.553 @@ -3866,7 +3851,7 @@
   1.554    proof- fix x assume "f x \<in> T" hence "f x \<in> f ` s" using as by auto
   1.555      thus "x \<in> s" unfolding inj_image_mem_iff[OF assms(2)] . qed auto qed
   1.556  
   1.557 -text{* Equality of continuous functions on closure and related results.          *}
   1.558 +text {* Equality of continuous functions on closure and related results. *}
   1.559  
   1.560  lemma continuous_closed_in_preimage_constant:
   1.561    fixes f :: "_ \<Rightarrow> 'b::t1_space"
   1.562 @@ -3909,7 +3894,7 @@
   1.563      unfolding subset_eq apply(erule_tac x="f x" in ballE) by (auto simp add: dist_norm)
   1.564  qed
   1.565  
   1.566 -text{* Making a continuous function avoid some value in a neighbourhood.         *}
   1.567 +text {* Making a continuous function avoid some value in a neighbourhood. *}
   1.568  
   1.569  lemma continuous_within_avoid:
   1.570    fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
   1.571 @@ -3942,7 +3927,7 @@
   1.572    shows "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> f y \<noteq> a"
   1.573  using assms(1)[unfolded continuous_on_eq_continuous_at[OF assms(2)], THEN bspec[where x=x], OF assms(3)]  continuous_at_avoid[of x f a]  assms(3,4) by auto
   1.574  
   1.575 -text{* Proving a function is constant by proving open-ness of level set.         *}
   1.576 +text {* Proving a function is constant by proving open-ness of level set. *}
   1.577  
   1.578  lemma continuous_levelset_open_in_cases:
   1.579    fixes f :: "_ \<Rightarrow> 'b::t1_space"
   1.580 @@ -3965,7 +3950,7 @@
   1.581    shows "\<forall>x \<in> s. f x = a"
   1.582  using continuous_levelset_open_in[OF assms(1,2), of a, unfolded openin_open] using assms (3,4) by fast
   1.583  
   1.584 -text{* Some arithmetical combinations (more to prove).                           *}
   1.585 +text {* Some arithmetical combinations (more to prove). *}
   1.586  
   1.587  lemma open_scaling[intro]:
   1.588    fixes s :: "'a::real_normed_vector set"
   1.589 @@ -4034,7 +4019,7 @@
   1.590    thus "x \<in> interior (op + a ` s)" unfolding mem_interior using `e>0` by auto
   1.591  qed
   1.592  
   1.593 -text {* We can now extend limit compositions to consider the scalar multiplier.   *}
   1.594 +text {* We can now extend limit compositions to consider the scalar multiplier. *}
   1.595  
   1.596  lemma continuous_vmul:
   1.597    fixes c :: "'a::metric_space \<Rightarrow> real" and v :: "'b::real_normed_vector"
   1.598 @@ -4078,7 +4063,7 @@
   1.599    uniformly_continuous_on_cmul uniformly_continuous_on_neg
   1.600    uniformly_continuous_on_sub
   1.601  
   1.602 -text{* And so we have continuity of inverse.                                     *}
   1.603 +text {* And so we have continuity of inverse. *}
   1.604  
   1.605  lemma continuous_inv:
   1.606    fixes f :: "'a::metric_space \<Rightarrow> real"
   1.607 @@ -4125,7 +4110,7 @@
   1.608    shows "bounded_linear f ==> continuous_on s f"
   1.609    using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto
   1.610  
   1.611 -text{* Also bilinear functions, in composition form.                             *}
   1.612 +text {* Also bilinear functions, in composition form. *}
   1.613  
   1.614  lemma bilinear_continuous_at_compose:
   1.615    shows "continuous (at x) f \<Longrightarrow> continuous (at x) g \<Longrightarrow> bounded_bilinear h
   1.616 @@ -4143,7 +4128,7 @@
   1.617    unfolding continuous_on_def
   1.618    by (fast elim: bounded_bilinear.tendsto)
   1.619  
   1.620 -text {* Preservation of compactness and connectedness under continuous function.  *}
   1.621 +text {* Preservation of compactness and connectedness under continuous function. *}
   1.622  
   1.623  lemma compact_continuous_image:
   1.624    assumes "continuous_on s f"  "compact s"
   1.625 @@ -4175,7 +4160,7 @@
   1.626    thus ?thesis unfolding connected_clopen by auto
   1.627  qed
   1.628  
   1.629 -text{* Continuity implies uniform continuity on a compact domain.                *}
   1.630 +text {* Continuity implies uniform continuity on a compact domain. *}
   1.631  
   1.632  lemma compact_uniformly_continuous:
   1.633    assumes "continuous_on s f"  "compact s"
   1.634 @@ -4265,8 +4250,8 @@
   1.635    thus ?thesis unfolding continuous_on_iff by auto
   1.636  qed
   1.637  
   1.638 -subsection{* Topological stuff lifted from and dropped to R                            *}
   1.639 -
   1.640 +
   1.641 +subsection {* Topological stuff lifted from and dropped to R *}
   1.642  
   1.643  lemma open_real:
   1.644    fixes s :: "real set" shows
   1.645 @@ -4311,7 +4296,7 @@
   1.646    apply auto apply (rule_tac x=e in exI) apply auto
   1.647    using order_trans[OF real_abs_sub_infnorm infnorm_le_norm, of _ x] by (metis xt1(7))
   1.648  
   1.649 -text{* Hence some handy theorems on distance, diameter etc. of/from a set.       *}
   1.650 +text {* Hence some handy theorems on distance, diameter etc. of/from a set. *}
   1.651  
   1.652  lemma compact_attains_sup:
   1.653    fixes s :: "real set"
   1.654 @@ -4376,7 +4361,7 @@
   1.655      unfolding continuous_on ..
   1.656  qed
   1.657  
   1.658 -text{* For *minimal* distance, we only need closure, not compactness.            *}
   1.659 +text {* For \emph{minimal} distance, we only need closure, not compactness. *}
   1.660  
   1.661  lemma distance_attains_inf:
   1.662    fixes a :: "'a::heine_borel"
   1.663 @@ -4412,6 +4397,7 @@
   1.664    thus ?thesis by fastsimp
   1.665  qed
   1.666  
   1.667 +
   1.668  subsection {* Pasted sets *}
   1.669  
   1.670  lemma bounded_Times:
   1.671 @@ -4444,7 +4430,7 @@
   1.672  apply (simp add: o_def)
   1.673  done
   1.674  
   1.675 -text{* Hence some useful properties follow quite easily.                         *}
   1.676 +text{* Hence some useful properties follow quite easily. *}
   1.677  
   1.678  lemma compact_scaling:
   1.679    fixes s :: "'a::real_normed_vector set"
   1.680 @@ -4497,7 +4483,7 @@
   1.681    thus ?thesis using compact_translation[OF compact_scaling[OF assms], of a c] by auto
   1.682  qed
   1.683  
   1.684 -text{* Hence we get the following.                                               *}
   1.685 +text {* Hence we get the following. *}
   1.686  
   1.687  lemma compact_sup_maxdistance:
   1.688    fixes s :: "'a::real_normed_vector set"
   1.689 @@ -4512,7 +4498,7 @@
   1.690    thus ?thesis using x(2)[unfolded `x = a - b`] by blast
   1.691  qed
   1.692  
   1.693 -text{* We can state this in terms of diameter of a set.                          *}
   1.694 +text {* We can state this in terms of diameter of a set. *}
   1.695  
   1.696  definition "diameter s = (if s = {} then 0::real else Sup {norm(x - y) | x y. x \<in> s \<and> y \<in> s})"
   1.697    (* TODO: generalize to class metric_space *)
   1.698 @@ -4565,7 +4551,7 @@
   1.699      by (metis b diameter_bounded_bound order_antisym xys)
   1.700  qed
   1.701  
   1.702 -text{* Related results with closure as the conclusion.                           *}
   1.703 +text {* Related results with closure as the conclusion. *}
   1.704  
   1.705  lemma closed_scaling:
   1.706    fixes s :: "'a::real_normed_vector set"
   1.707 @@ -4693,7 +4679,8 @@
   1.708    shows "frontier((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (frontier s)"
   1.709    unfolding frontier_def translation_diff interior_translation closure_translation by auto
   1.710  
   1.711 -subsection{* Separation between points and sets.                                       *}
   1.712 +
   1.713 +subsection {* Separation between points and sets *}
   1.714  
   1.715  lemma separate_point_closed:
   1.716    fixes s :: "'a::heine_borel set"
   1.717 @@ -4736,6 +4723,7 @@
   1.718      by (auto simp add: dist_commute)
   1.719  qed
   1.720  
   1.721 +
   1.722  subsection {* Intervals *}
   1.723    
   1.724  lemma interval: fixes a :: "'a::ordered_euclidean_space" shows
   1.725 @@ -5168,7 +5156,8 @@
   1.726    unfolding is_interval_def
   1.727    by simp
   1.728  
   1.729 -subsection{* Closure of halfspaces and hyperplanes.                                    *}
   1.730 +
   1.731 +subsection {* Closure of halfspaces and hyperplanes *}
   1.732  
   1.733  lemma Lim_inner:
   1.734    assumes "(f ---> l) net"  shows "((\<lambda>y. inner a (f y)) ---> inner a l) net"
   1.735 @@ -5212,7 +5201,7 @@
   1.736    shows "closed {x::'a::euclidean_space. x$$i \<ge> a}"
   1.737    using closed_halfspace_ge[of a "(basis i)::'a"] unfolding euclidean_component_def .
   1.738  
   1.739 -text{* Openness of halfspaces.                                                   *}
   1.740 +text {* Openness of halfspaces. *}
   1.741  
   1.742  lemma open_halfspace_lt: "open {x. inner a x < b}"
   1.743  proof-
   1.744 @@ -5291,7 +5280,7 @@
   1.745  lemma open_vimage_euclidean_component: "open S \<Longrightarrow> open ((\<lambda>x. x $$ i) -` S)"
   1.746    by (auto intro!: continuous_open_vimage)
   1.747  
   1.748 -text{* This gives a simple derivation of limit component bounds.                 *}
   1.749 +text {* This gives a simple derivation of limit component bounds. *}
   1.750  
   1.751  lemma Lim_component_le: fixes f :: "'a \<Rightarrow> 'b::euclidean_space"
   1.752    assumes "(f ---> l) net" "\<not> (trivial_limit net)"  "eventually (\<lambda>x. f(x)$$i \<le> b) net"
   1.753 @@ -5378,6 +5367,7 @@
   1.754    using connected_ivt_hyperplane[of s x y "(basis k)::'a" a]
   1.755    unfolding euclidean_component_def by auto
   1.756  
   1.757 +
   1.758  subsection {* Homeomorphisms *}
   1.759  
   1.760  definition "homeomorphism s t f g \<equiv>
   1.761 @@ -5642,7 +5632,8 @@
   1.762      unfolding complete_eq_closed[THEN sym] by auto
   1.763  qed
   1.764  
   1.765 -subsection{* Some properties of a canonical subspace.                                  *}
   1.766 +
   1.767 +subsection {* Some properties of a canonical subspace *}
   1.768  
   1.769  (** move **)
   1.770  declare euclidean_component.zero[simp]  
   1.771 @@ -5767,6 +5758,7 @@
   1.772    thus ?thesis using dim_subset[OF closure_subset, of s] by auto
   1.773  qed
   1.774  
   1.775 +
   1.776  subsection {* Affine transformations of intervals *}
   1.777  
   1.778  lemma real_affinity_le:
   1.779 @@ -5837,7 +5829,8 @@
   1.780    (if {a..b} = {} then {} else if 0 \<le> m then {m *\<^sub>R a..m *\<^sub>R b} else {m *\<^sub>R b..m *\<^sub>R a})"
   1.781    using image_affinity_interval[of m 0 a b] by auto
   1.782  
   1.783 -subsection{* Banach fixed point theorem (not really topological...) *}
   1.784 +
   1.785 +subsection {* Banach fixed point theorem (not really topological...) *}
   1.786  
   1.787  lemma banach_fix:
   1.788    assumes s:"complete s" "s \<noteq> {}" and c:"0 \<le> c" "c < 1" and f:"(f ` s) \<subseteq> s" and
   1.789 @@ -5967,7 +5960,7 @@
   1.790    ultimately show ?thesis using `x\<in>s` by blast+
   1.791  qed
   1.792  
   1.793 -subsection{* Edelstein fixed point theorem.                                            *}
   1.794 +subsection {* Edelstein fixed point theorem *}
   1.795  
   1.796  lemma edelstein_fix:
   1.797    fixes s :: "'a::real_normed_vector set"