src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
 changeset 44210 eba74571833b parent 44207 ea99698c2070 child 44211 bd7c586b902e
     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"