--- a/src/HOL/Analysis/Connected.thy Sun Jan 06 16:27:52 2019 +0100
+++ b/src/HOL/Analysis/Connected.thy Sun Jan 06 17:54:49 2019 +0100
@@ -10,342 +10,60 @@
Topology_Euclidean_Space
begin
-subsection%unimportant \<open>More properties of closed balls, spheres, etc\<close>
-
-lemma mem_interior_cball: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. cball x e \<subseteq> S)"
- apply (simp add: interior_def, safe)
- apply (force simp: open_contains_cball)
- apply (rule_tac x="ball x e" in exI)
- apply (simp add: subset_trans [OF ball_subset_cball])
- done
-
-lemma islimpt_ball:
- fixes x y :: "'a::{real_normed_vector,perfect_space}"
- shows "y islimpt ball x e \<longleftrightarrow> 0 < e \<and> y \<in> cball x e"
- (is "?lhs \<longleftrightarrow> ?rhs")
-proof
- show ?rhs if ?lhs
- proof
- {
- assume "e \<le> 0"
- then have *: "ball x e = {}"
- using ball_eq_empty[of x e] by auto
- have False using \<open>?lhs\<close>
- unfolding * using islimpt_EMPTY[of y] by auto
- }
- then show "e > 0" by (metis not_less)
- show "y \<in> cball x e"
- using closed_cball[of x e] islimpt_subset[of y "ball x e" "cball x e"]
- ball_subset_cball[of x e] \<open>?lhs\<close>
- unfolding closed_limpt by auto
+subsection%unimportant\<open>Lemmas Combining Imports\<close>
+
+lemma isCont_indicator:
+ fixes x :: "'a::t2_space"
+ shows "isCont (indicator A :: 'a \<Rightarrow> real) x = (x \<notin> frontier A)"
+proof auto
+ fix x
+ assume cts_at: "isCont (indicator A :: 'a \<Rightarrow> real) x" and fr: "x \<in> frontier A"
+ with continuous_at_open have 1: "\<forall>V::real set. open V \<and> indicator A x \<in> V \<longrightarrow>
+ (\<exists>U::'a set. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> V))" by auto
+ show False
+ proof (cases "x \<in> A")
+ assume x: "x \<in> A"
+ hence "indicator A x \<in> ({0<..<2} :: real set)" by simp
+ hence "\<exists>U. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> ({0<..<2} :: real set))"
+ using 1 open_greaterThanLessThan by blast
+ then guess U .. note U = this
+ hence "\<forall>y\<in>U. indicator A y > (0::real)"
+ unfolding greaterThanLessThan_def by auto
+ hence "U \<subseteq> A" using indicator_eq_0_iff by force
+ hence "x \<in> interior A" using U interiorI by auto
+ thus ?thesis using fr unfolding frontier_def by simp
+ next
+ assume x: "x \<notin> A"
+ hence "indicator A x \<in> ({-1<..<1} :: real set)" by simp
+ hence "\<exists>U. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> ({-1<..<1} :: real set))"
+ using 1 open_greaterThanLessThan by blast
+ then guess U .. note U = this
+ hence "\<forall>y\<in>U. indicator A y < (1::real)"
+ unfolding greaterThanLessThan_def by auto
+ hence "U \<subseteq> -A" by auto
+ hence "x \<in> interior (-A)" using U interiorI by auto
+ thus ?thesis using fr interior_complement unfolding frontier_def by auto
qed
- show ?lhs if ?rhs
- proof -
- from that have "e > 0" by auto
- {
- fix d :: real
- assume "d > 0"
- have "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
- proof (cases "d \<le> dist x y")
- case True
- then show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
- proof (cases "x = y")
- case True
- then have False
- using \<open>d \<le> dist x y\<close> \<open>d>0\<close> by auto
- then show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
- by auto
- next
- case False
- have "dist x (y - (d / (2 * dist y x)) *\<^sub>R (y - x)) =
- norm (x - y + (d / (2 * norm (y - x))) *\<^sub>R (y - x))"
- unfolding mem_cball mem_ball dist_norm diff_diff_eq2 diff_add_eq[symmetric]
- by auto
- also have "\<dots> = \<bar>- 1 + d / (2 * norm (x - y))\<bar> * norm (x - y)"
- using scaleR_left_distrib[of "- 1" "d / (2 * norm (y - x))", symmetric, of "y - x"]
- unfolding scaleR_minus_left scaleR_one
- by (auto simp: norm_minus_commute)
- also have "\<dots> = \<bar>- norm (x - y) + d / 2\<bar>"
- unfolding abs_mult_pos[of "norm (x - y)", OF norm_ge_zero[of "x - y"]]
- unfolding distrib_right using \<open>x\<noteq>y\<close> by auto
- also have "\<dots> \<le> e - d/2" using \<open>d \<le> dist x y\<close> and \<open>d>0\<close> and \<open>?rhs\<close>
- by (auto simp: dist_norm)
- finally have "y - (d / (2 * dist y x)) *\<^sub>R (y - x) \<in> ball x e" using \<open>d>0\<close>
- by auto
- moreover
- have "(d / (2*dist y x)) *\<^sub>R (y - x) \<noteq> 0"
- using \<open>x\<noteq>y\<close>[unfolded dist_nz] \<open>d>0\<close> unfolding scaleR_eq_0_iff
- by (auto simp: dist_commute)
- moreover
- have "dist (y - (d / (2 * dist y x)) *\<^sub>R (y - x)) y < d"
- unfolding dist_norm
- apply simp
- unfolding norm_minus_cancel
- using \<open>d > 0\<close> \<open>x\<noteq>y\<close>[unfolded dist_nz] dist_commute[of x y]
- unfolding dist_norm
- apply auto
- done
- ultimately show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
- apply (rule_tac x = "y - (d / (2*dist y x)) *\<^sub>R (y - x)" in bexI)
- apply auto
- done
- qed
- next
- case False
- then have "d > dist x y" by auto
- show "\<exists>x' \<in> ball x e. x' \<noteq> y \<and> dist x' y < d"
- proof (cases "x = y")
- case True
- obtain z where **: "z \<noteq> y" "dist z y < min e d"
- using perfect_choose_dist[of "min e d" y]
- using \<open>d > 0\<close> \<open>e>0\<close> by auto
- show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
- unfolding \<open>x = y\<close>
- using \<open>z \<noteq> y\<close> **
- apply (rule_tac x=z in bexI)
- apply (auto simp: dist_commute)
- done
- next
- case False
- then show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
- using \<open>d>0\<close> \<open>d > dist x y\<close> \<open>?rhs\<close>
- apply (rule_tac x=x in bexI, auto)
- done
- qed
- qed
- }
- then show ?thesis
- unfolding mem_cball islimpt_approachable mem_ball by auto
+next
+ assume nfr: "x \<notin> frontier A"
+ hence "x \<in> interior A \<or> x \<in> interior (-A)"
+ by (auto simp: frontier_def closure_interior)
+ thus "isCont ((indicator A)::'a \<Rightarrow> real) x"
+ proof
+ assume int: "x \<in> interior A"
+ then obtain U where U: "open U" "x \<in> U" "U \<subseteq> A" unfolding interior_def by auto
+ hence "\<forall>y\<in>U. indicator A y = (1::real)" unfolding indicator_def by auto
+ hence "continuous_on U (indicator A)" by (simp add: continuous_on_const indicator_eq_1_iff)
+ thus ?thesis using U continuous_on_eq_continuous_at by auto
+ next
+ assume ext: "x \<in> interior (-A)"
+ then obtain U where U: "open U" "x \<in> U" "U \<subseteq> -A" unfolding interior_def by auto
+ then have "continuous_on U (indicator A)"
+ using continuous_on_topological by (auto simp: subset_iff)
+ thus ?thesis using U continuous_on_eq_continuous_at by auto
qed
qed
-lemma closure_ball_lemma:
- fixes x y :: "'a::real_normed_vector"
- assumes "x \<noteq> y"
- shows "y islimpt ball x (dist x y)"
-proof (rule islimptI)
- fix T
- assume "y \<in> T" "open T"
- then obtain r where "0 < r" "\<forall>z. dist z y < r \<longrightarrow> z \<in> T"
- unfolding open_dist by fast
- (* choose point between x and y, within distance r of y. *)
- define k where "k = min 1 (r / (2 * dist x y))"
- define z where "z = y + scaleR k (x - y)"
- have z_def2: "z = x + scaleR (1 - k) (y - x)"
- unfolding z_def by (simp add: algebra_simps)
- have "dist z y < r"
- unfolding z_def k_def using \<open>0 < r\<close>
- by (simp add: dist_norm min_def)
- then have "z \<in> T"
- using \<open>\<forall>z. dist z y < r \<longrightarrow> z \<in> T\<close> by simp
- have "dist x z < dist x y"
- unfolding z_def2 dist_norm
- apply (simp add: norm_minus_commute)
- apply (simp only: dist_norm [symmetric])
- apply (subgoal_tac "\<bar>1 - k\<bar> * dist x y < 1 * dist x y", simp)
- apply (rule mult_strict_right_mono)
- apply (simp add: k_def \<open>0 < r\<close> \<open>x \<noteq> y\<close>)
- apply (simp add: \<open>x \<noteq> y\<close>)
- done
- then have "z \<in> ball x (dist x y)"
- by simp
- have "z \<noteq> y"
- unfolding z_def k_def using \<open>x \<noteq> y\<close> \<open>0 < r\<close>
- by (simp add: min_def)
- show "\<exists>z\<in>ball x (dist x y). z \<in> T \<and> z \<noteq> y"
- using \<open>z \<in> ball x (dist x y)\<close> \<open>z \<in> T\<close> \<open>z \<noteq> y\<close>
- by fast
-qed
-
-lemma at_within_ball_bot_iff:
- fixes x y :: "'a::{real_normed_vector,perfect_space}"
- shows "at x within ball y r = bot \<longleftrightarrow> (r=0 \<or> x \<notin> cball y r)"
- unfolding trivial_limit_within
-apply (auto simp add:trivial_limit_within islimpt_ball )
-by (metis le_less_trans less_eq_real_def zero_le_dist)
-
-lemma closure_ball [simp]:
- fixes x :: "'a::real_normed_vector"
- shows "0 < e \<Longrightarrow> closure (ball x e) = cball x e"
- apply (rule equalityI)
- apply (rule closure_minimal)
- apply (rule ball_subset_cball)
- apply (rule closed_cball)
- apply (rule subsetI, rename_tac y)
- apply (simp add: le_less [where 'a=real])
- apply (erule disjE)
- apply (rule subsetD [OF closure_subset], simp)
- apply (simp add: closure_def, clarify)
- apply (rule closure_ball_lemma)
- apply simp
- done
-
-(* In a trivial vector space, this fails for e = 0. *)
-lemma interior_cball [simp]:
- fixes x :: "'a::{real_normed_vector, perfect_space}"
- shows "interior (cball x e) = ball x e"
-proof (cases "e \<ge> 0")
- case False note cs = this
- from cs have null: "ball x e = {}"
- using ball_empty[of e x] by auto
- moreover
- {
- fix y
- assume "y \<in> cball x e"
- then have False
- by (metis ball_eq_empty null cs dist_eq_0_iff dist_le_zero_iff empty_subsetI mem_cball subset_antisym subset_ball)
- }
- then have "cball x e = {}" by auto
- then have "interior (cball x e) = {}"
- using interior_empty by auto
- ultimately show ?thesis by blast
-next
- case True note cs = this
- have "ball x e \<subseteq> cball x e"
- using ball_subset_cball by auto
- moreover
- {
- fix S y
- assume as: "S \<subseteq> cball x e" "open S" "y\<in>S"
- then obtain d where "d>0" and d: "\<forall>x'. dist x' y < d \<longrightarrow> x' \<in> S"
- unfolding open_dist by blast
- then obtain xa where xa_y: "xa \<noteq> y" and xa: "dist xa y < d"
- using perfect_choose_dist [of d] by auto
- have "xa \<in> S"
- using d[THEN spec[where x = xa]]
- using xa by (auto simp: dist_commute)
- then have xa_cball: "xa \<in> cball x e"
- using as(1) by auto
- then have "y \<in> ball x e"
- proof (cases "x = y")
- case True
- then have "e > 0" using cs order.order_iff_strict xa_cball xa_y by fastforce
- then show "y \<in> ball x e"
- using \<open>x = y \<close> by simp
- next
- case False
- have "dist (y + (d / 2 / dist y x) *\<^sub>R (y - x)) y < d"
- unfolding dist_norm
- using \<open>d>0\<close> norm_ge_zero[of "y - x"] \<open>x \<noteq> y\<close> by auto
- then have *: "y + (d / 2 / dist y x) *\<^sub>R (y - x) \<in> cball x e"
- using d as(1)[unfolded subset_eq] by blast
- have "y - x \<noteq> 0" using \<open>x \<noteq> y\<close> by auto
- hence **:"d / (2 * norm (y - x)) > 0"
- unfolding zero_less_norm_iff[symmetric] using \<open>d>0\<close> by auto
- have "dist (y + (d / 2 / dist y x) *\<^sub>R (y - x)) x =
- norm (y + (d / (2 * norm (y - x))) *\<^sub>R y - (d / (2 * norm (y - x))) *\<^sub>R x - x)"
- by (auto simp: dist_norm algebra_simps)
- also have "\<dots> = norm ((1 + d / (2 * norm (y - x))) *\<^sub>R (y - x))"
- by (auto simp: algebra_simps)
- also have "\<dots> = \<bar>1 + d / (2 * norm (y - x))\<bar> * norm (y - x)"
- using ** by auto
- also have "\<dots> = (dist y x) + d/2"
- using ** by (auto simp: distrib_right dist_norm)
- finally have "e \<ge> dist x y +d/2"
- using *[unfolded mem_cball] by (auto simp: dist_commute)
- then show "y \<in> ball x e"
- unfolding mem_ball using \<open>d>0\<close> by auto
- qed
- }
- then have "\<forall>S \<subseteq> cball x e. open S \<longrightarrow> S \<subseteq> ball x e"
- by auto
- ultimately show ?thesis
- using interior_unique[of "ball x e" "cball x e"]
- using open_ball[of x e]
- by auto
-qed
-
-lemma interior_ball [simp]: "interior (ball x e) = ball x e"
- by (simp add: interior_open)
-
-lemma frontier_ball [simp]:
- fixes a :: "'a::real_normed_vector"
- shows "0 < e \<Longrightarrow> frontier (ball a e) = sphere a e"
- by (force simp: frontier_def)
-
-lemma frontier_cball [simp]:
- fixes a :: "'a::{real_normed_vector, perfect_space}"
- shows "frontier (cball a e) = sphere a e"
- by (force simp: frontier_def)
-
-lemma cball_eq_empty [simp]: "cball x e = {} \<longleftrightarrow> e < 0"
- apply (simp add: set_eq_iff not_le)
- apply (metis zero_le_dist dist_self order_less_le_trans)
- done
-
-lemma cball_empty [simp]: "e < 0 \<Longrightarrow> cball x e = {}"
- by simp
-
-lemma cball_eq_sing:
- fixes x :: "'a::{metric_space,perfect_space}"
- shows "cball x e = {x} \<longleftrightarrow> e = 0"
-proof (rule linorder_cases)
- assume e: "0 < e"
- obtain a where "a \<noteq> x" "dist a x < e"
- using perfect_choose_dist [OF e] by auto
- then have "a \<noteq> x" "dist x a \<le> e"
- by (auto simp: dist_commute)
- with e show ?thesis by (auto simp: set_eq_iff)
-qed auto
-
-lemma cball_sing:
- fixes x :: "'a::metric_space"
- shows "e = 0 \<Longrightarrow> cball x e = {x}"
- by (auto simp: set_eq_iff)
-
-lemma ball_divide_subset: "d \<ge> 1 \<Longrightarrow> ball x (e/d) \<subseteq> ball x e"
- apply (cases "e \<le> 0")
- apply (simp add: ball_empty divide_simps)
- apply (rule subset_ball)
- apply (simp add: divide_simps)
- done
-
-lemma ball_divide_subset_numeral: "ball x (e / numeral w) \<subseteq> ball x e"
- using ball_divide_subset one_le_numeral by blast
-
-lemma cball_divide_subset: "d \<ge> 1 \<Longrightarrow> cball x (e/d) \<subseteq> cball x e"
- apply (cases "e < 0")
- apply (simp add: divide_simps)
- apply (rule subset_cball)
- apply (metis div_by_1 frac_le not_le order_refl zero_less_one)
- done
-
-lemma cball_divide_subset_numeral: "cball x (e / numeral w) \<subseteq> cball x e"
- using cball_divide_subset one_le_numeral by blast
-
-lemma compact_cball[simp]:
- fixes x :: "'a::heine_borel"
- shows "compact (cball x e)"
- using compact_eq_bounded_closed bounded_cball closed_cball
- by blast
-
-lemma compact_frontier_bounded[intro]:
- fixes S :: "'a::heine_borel set"
- shows "bounded S \<Longrightarrow> compact (frontier S)"
- unfolding frontier_def
- using compact_eq_bounded_closed
- by blast
-
-lemma compact_frontier[intro]:
- fixes S :: "'a::heine_borel set"
- shows "compact S \<Longrightarrow> compact (frontier S)"
- using compact_eq_bounded_closed compact_frontier_bounded
- by blast
-
-corollary compact_sphere [simp]:
- fixes a :: "'a::{real_normed_vector,perfect_space,heine_borel}"
- shows "compact (sphere a r)"
-using compact_frontier [of "cball a r"] by simp
-
-corollary bounded_sphere [simp]:
- fixes a :: "'a::{real_normed_vector,perfect_space,heine_borel}"
- shows "bounded (sphere a r)"
-by (simp add: compact_imp_bounded)
-
-corollary closed_sphere [simp]:
- fixes a :: "'a::{real_normed_vector,perfect_space,heine_borel}"
- shows "closed (sphere a r)"
-by (simp add: compact_imp_closed)
subsection%unimportant \<open>Connectedness\<close>
@@ -776,1325 +494,6 @@
using closedin_connected_component componentsE by blast
-subsection \<open>Intersecting chains of compact sets and the Baire property\<close>
-
-proposition bounded_closed_chain:
- fixes \<F> :: "'a::heine_borel set set"
- assumes "B \<in> \<F>" "bounded B" and \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> closed S" and "{} \<notin> \<F>"
- and chain: "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
- shows "\<Inter>\<F> \<noteq> {}"
-proof -
- have "B \<inter> \<Inter>\<F> \<noteq> {}"
- proof (rule compact_imp_fip)
- show "compact B" "\<And>T. T \<in> \<F> \<Longrightarrow> closed T"
- by (simp_all add: assms compact_eq_bounded_closed)
- show "\<lbrakk>finite \<G>; \<G> \<subseteq> \<F>\<rbrakk> \<Longrightarrow> B \<inter> \<Inter>\<G> \<noteq> {}" for \<G>
- proof (induction \<G> rule: finite_induct)
- case empty
- with assms show ?case by force
- next
- case (insert U \<G>)
- then have "U \<in> \<F>" and ne: "B \<inter> \<Inter>\<G> \<noteq> {}" by auto
- then consider "B \<subseteq> U" | "U \<subseteq> B"
- using \<open>B \<in> \<F>\<close> chain by blast
- then show ?case
- proof cases
- case 1
- then show ?thesis
- using Int_left_commute ne by auto
- next
- case 2
- have "U \<noteq> {}"
- using \<open>U \<in> \<F>\<close> \<open>{} \<notin> \<F>\<close> by blast
- moreover
- have False if "\<And>x. x \<in> U \<Longrightarrow> \<exists>Y\<in>\<G>. x \<notin> Y"
- proof -
- have "\<And>x. x \<in> U \<Longrightarrow> \<exists>Y\<in>\<G>. Y \<subseteq> U"
- by (metis chain contra_subsetD insert.prems insert_subset that)
- then obtain Y where "Y \<in> \<G>" "Y \<subseteq> U"
- by (metis all_not_in_conv \<open>U \<noteq> {}\<close>)
- moreover obtain x where "x \<in> \<Inter>\<G>"
- by (metis Int_emptyI ne)
- ultimately show ?thesis
- by (metis Inf_lower subset_eq that)
- qed
- with 2 show ?thesis
- by blast
- qed
- qed
- qed
- then show ?thesis by blast
-qed
-
-corollary compact_chain:
- fixes \<F> :: "'a::heine_borel set set"
- assumes "\<And>S. S \<in> \<F> \<Longrightarrow> compact S" "{} \<notin> \<F>"
- "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
- shows "\<Inter> \<F> \<noteq> {}"
-proof (cases "\<F> = {}")
- case True
- then show ?thesis by auto
-next
- case False
- show ?thesis
- by (metis False all_not_in_conv assms compact_imp_bounded compact_imp_closed bounded_closed_chain)
-qed
-
-lemma compact_nest:
- fixes F :: "'a::linorder \<Rightarrow> 'b::heine_borel set"
- assumes F: "\<And>n. compact(F n)" "\<And>n. F n \<noteq> {}" and mono: "\<And>m n. m \<le> n \<Longrightarrow> F n \<subseteq> F m"
- shows "\<Inter>range F \<noteq> {}"
-proof -
- have *: "\<And>S T. S \<in> range F \<and> T \<in> range F \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
- by (metis mono image_iff le_cases)
- show ?thesis
- apply (rule compact_chain [OF _ _ *])
- using F apply (blast intro: dest: *)+
- done
-qed
-
-text\<open>The Baire property of dense sets\<close>
-theorem Baire:
- fixes S::"'a::{real_normed_vector,heine_borel} set"
- assumes "closed S" "countable \<G>"
- and ope: "\<And>T. T \<in> \<G> \<Longrightarrow> openin (subtopology euclidean S) T \<and> S \<subseteq> closure T"
- shows "S \<subseteq> closure(\<Inter>\<G>)"
-proof (cases "\<G> = {}")
- case True
- then show ?thesis
- using closure_subset by auto
-next
- let ?g = "from_nat_into \<G>"
- case False
- then have gin: "?g n \<in> \<G>" for n
- by (simp add: from_nat_into)
- show ?thesis
- proof (clarsimp simp: closure_approachable)
- fix x and e::real
- assume "x \<in> S" "0 < e"
- obtain TF where opeF: "\<And>n. openin (subtopology euclidean S) (TF n)"
- and ne: "\<And>n. TF n \<noteq> {}"
- and subg: "\<And>n. S \<inter> closure(TF n) \<subseteq> ?g n"
- and subball: "\<And>n. closure(TF n) \<subseteq> ball x e"
- and decr: "\<And>n. TF(Suc n) \<subseteq> TF n"
- proof -
- have *: "\<exists>Y. (openin (subtopology euclidean S) Y \<and> Y \<noteq> {} \<and>
- S \<inter> closure Y \<subseteq> ?g n \<and> closure Y \<subseteq> ball x e) \<and> Y \<subseteq> U"
- if opeU: "openin (subtopology euclidean S) U" and "U \<noteq> {}" and cloU: "closure U \<subseteq> ball x e" for U n
- proof -
- obtain T where T: "open T" "U = T \<inter> S"
- using \<open>openin (subtopology euclidean S) U\<close> by (auto simp: openin_subtopology)
- with \<open>U \<noteq> {}\<close> have "T \<inter> closure (?g n) \<noteq> {}"
- using gin ope by fastforce
- then have "T \<inter> ?g n \<noteq> {}"
- using \<open>open T\<close> open_Int_closure_eq_empty by blast
- then obtain y where "y \<in> U" "y \<in> ?g n"
- using T ope [of "?g n", OF gin] by (blast dest: openin_imp_subset)
- moreover have "openin (subtopology euclidean S) (U \<inter> ?g n)"
- using gin ope opeU by blast
- ultimately obtain d where U: "U \<inter> ?g n \<subseteq> S" and "d > 0" and d: "ball y d \<inter> S \<subseteq> U \<inter> ?g n"
- by (force simp: openin_contains_ball)
- show ?thesis
- proof (intro exI conjI)
- show "openin (subtopology euclidean S) (S \<inter> ball y (d/2))"
- by (simp add: openin_open_Int)
- show "S \<inter> ball y (d/2) \<noteq> {}"
- using \<open>0 < d\<close> \<open>y \<in> U\<close> opeU openin_imp_subset by fastforce
- have "S \<inter> closure (S \<inter> ball y (d/2)) \<subseteq> S \<inter> closure (ball y (d/2))"
- using closure_mono by blast
- also have "... \<subseteq> ?g n"
- using \<open>d > 0\<close> d by force
- finally show "S \<inter> closure (S \<inter> ball y (d/2)) \<subseteq> ?g n" .
- have "closure (S \<inter> ball y (d/2)) \<subseteq> S \<inter> ball y d"
- proof -
- have "closure (ball y (d/2)) \<subseteq> ball y d"
- using \<open>d > 0\<close> by auto
- then have "closure (S \<inter> ball y (d/2)) \<subseteq> ball y d"
- by (meson closure_mono inf.cobounded2 subset_trans)
- then show ?thesis
- by (simp add: \<open>closed S\<close> closure_minimal)
- qed
- also have "... \<subseteq> ball x e"
- using cloU closure_subset d by blast
- finally show "closure (S \<inter> ball y (d/2)) \<subseteq> ball x e" .
- show "S \<inter> ball y (d/2) \<subseteq> U"
- using ball_divide_subset_numeral d by blast
- qed
- qed
- let ?\<Phi> = "\<lambda>n X. openin (subtopology euclidean S) X \<and> X \<noteq> {} \<and>
- S \<inter> closure X \<subseteq> ?g n \<and> closure X \<subseteq> ball x e"
- have "closure (S \<inter> ball x (e / 2)) \<subseteq> closure(ball x (e/2))"
- by (simp add: closure_mono)
- also have "... \<subseteq> ball x e"
- using \<open>e > 0\<close> by auto
- finally have "closure (S \<inter> ball x (e / 2)) \<subseteq> ball x e" .
- moreover have"openin (subtopology euclidean S) (S \<inter> ball x (e / 2))" "S \<inter> ball x (e / 2) \<noteq> {}"
- using \<open>0 < e\<close> \<open>x \<in> S\<close> by auto
- ultimately obtain Y where Y: "?\<Phi> 0 Y \<and> Y \<subseteq> S \<inter> ball x (e / 2)"
- using * [of "S \<inter> ball x (e/2)" 0] by metis
- show thesis
- proof (rule exE [OF dependent_nat_choice [of ?\<Phi> "\<lambda>n X Y. Y \<subseteq> X"]])
- show "\<exists>x. ?\<Phi> 0 x"
- using Y by auto
- show "\<exists>Y. ?\<Phi> (Suc n) Y \<and> Y \<subseteq> X" if "?\<Phi> n X" for X n
- using that by (blast intro: *)
- qed (use that in metis)
- qed
- have "(\<Inter>n. S \<inter> closure (TF n)) \<noteq> {}"
- proof (rule compact_nest)
- show "\<And>n. compact (S \<inter> closure (TF n))"
- by (metis closed_closure subball bounded_subset_ballI compact_eq_bounded_closed closed_Int_compact [OF \<open>closed S\<close>])
- show "\<And>n. S \<inter> closure (TF n) \<noteq> {}"
- by (metis Int_absorb1 opeF \<open>closed S\<close> closure_eq_empty closure_minimal ne openin_imp_subset)
- show "\<And>m n. m \<le> n \<Longrightarrow> S \<inter> closure (TF n) \<subseteq> S \<inter> closure (TF m)"
- by (meson closure_mono decr dual_order.refl inf_mono lift_Suc_antimono_le)
- qed
- moreover have "(\<Inter>n. S \<inter> closure (TF n)) \<subseteq> {y \<in> \<Inter>\<G>. dist y x < e}"
- proof (clarsimp, intro conjI)
- fix y
- assume "y \<in> S" and y: "\<forall>n. y \<in> closure (TF n)"
- then show "\<forall>T\<in>\<G>. y \<in> T"
- by (metis Int_iff from_nat_into_surj [OF \<open>countable \<G>\<close>] set_mp subg)
- show "dist y x < e"
- by (metis y dist_commute mem_ball subball subsetCE)
- qed
- ultimately show "\<exists>y \<in> \<Inter>\<G>. dist y x < e"
- by auto
- qed
-qed
-
-subsection%unimportant \<open>Some theorems on sups and infs using the notion "bounded"\<close>
-
-lemma bounded_real: "bounded (S::real set) \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. \<bar>x\<bar> \<le> a)"
- by (simp add: bounded_iff)
-
-lemma bounded_imp_bdd_above: "bounded S \<Longrightarrow> bdd_above (S :: real set)"
- by (auto simp: bounded_def bdd_above_def dist_real_def)
- (metis abs_le_D1 abs_minus_commute diff_le_eq)
-
-lemma bounded_imp_bdd_below: "bounded S \<Longrightarrow> bdd_below (S :: real set)"
- by (auto simp: bounded_def bdd_below_def dist_real_def)
- (metis abs_le_D1 add.commute diff_le_eq)
-
-lemma bounded_inner_imp_bdd_above:
- assumes "bounded s"
- shows "bdd_above ((\<lambda>x. x \<bullet> a) ` s)"
-by (simp add: assms bounded_imp_bdd_above bounded_linear_image bounded_linear_inner_left)
-
-lemma bounded_inner_imp_bdd_below:
- assumes "bounded s"
- shows "bdd_below ((\<lambda>x. x \<bullet> a) ` s)"
-by (simp add: assms bounded_imp_bdd_below bounded_linear_image bounded_linear_inner_left)
-
-lemma bounded_has_Sup:
- fixes S :: "real set"
- assumes "bounded S"
- and "S \<noteq> {}"
- shows "\<forall>x\<in>S. x \<le> Sup S"
- and "\<forall>b. (\<forall>x\<in>S. x \<le> b) \<longrightarrow> Sup S \<le> b"
-proof
- show "\<forall>b. (\<forall>x\<in>S. x \<le> b) \<longrightarrow> Sup S \<le> b"
- using assms by (metis cSup_least)
-qed (metis cSup_upper assms(1) bounded_imp_bdd_above)
-
-lemma Sup_insert:
- fixes S :: "real set"
- shows "bounded S \<Longrightarrow> Sup (insert x S) = (if S = {} then x else max x (Sup S))"
- by (auto simp: bounded_imp_bdd_above sup_max cSup_insert_If)
-
-lemma Sup_insert_finite:
- fixes S :: "'a::conditionally_complete_linorder set"
- shows "finite S \<Longrightarrow> Sup (insert x S) = (if S = {} then x else max x (Sup S))"
-by (simp add: cSup_insert sup_max)
-
-lemma bounded_has_Inf:
- fixes S :: "real set"
- assumes "bounded S"
- and "S \<noteq> {}"
- shows "\<forall>x\<in>S. x \<ge> Inf S"
- and "\<forall>b. (\<forall>x\<in>S. x \<ge> b) \<longrightarrow> Inf S \<ge> b"
-proof
- show "\<forall>b. (\<forall>x\<in>S. x \<ge> b) \<longrightarrow> Inf S \<ge> b"
- using assms by (metis cInf_greatest)
-qed (metis cInf_lower assms(1) bounded_imp_bdd_below)
-
-lemma Inf_insert:
- fixes S :: "real set"
- shows "bounded S \<Longrightarrow> Inf (insert x S) = (if S = {} then x else min x (Inf S))"
- by (auto simp: bounded_imp_bdd_below inf_min cInf_insert_If)
-
-lemma Inf_insert_finite:
- fixes S :: "'a::conditionally_complete_linorder set"
- shows "finite S \<Longrightarrow> Inf (insert x S) = (if S = {} then x else min x (Inf S))"
-by (simp add: cInf_eq_Min)
-
-lemma finite_imp_less_Inf:
- fixes a :: "'a::conditionally_complete_linorder"
- shows "\<lbrakk>finite X; x \<in> X; \<And>x. x\<in>X \<Longrightarrow> a < x\<rbrakk> \<Longrightarrow> a < Inf X"
- by (induction X rule: finite_induct) (simp_all add: cInf_eq_Min Inf_insert_finite)
-
-lemma finite_less_Inf_iff:
- fixes a :: "'a :: conditionally_complete_linorder"
- shows "\<lbrakk>finite X; X \<noteq> {}\<rbrakk> \<Longrightarrow> a < Inf X \<longleftrightarrow> (\<forall>x \<in> X. a < x)"
- by (auto simp: cInf_eq_Min)
-
-lemma finite_imp_Sup_less:
- fixes a :: "'a::conditionally_complete_linorder"
- shows "\<lbrakk>finite X; x \<in> X; \<And>x. x\<in>X \<Longrightarrow> a > x\<rbrakk> \<Longrightarrow> a > Sup X"
- by (induction X rule: finite_induct) (simp_all add: cSup_eq_Max Sup_insert_finite)
-
-lemma finite_Sup_less_iff:
- fixes a :: "'a :: conditionally_complete_linorder"
- shows "\<lbrakk>finite X; X \<noteq> {}\<rbrakk> \<Longrightarrow> a > Sup X \<longleftrightarrow> (\<forall>x \<in> X. a > x)"
- by (auto simp: cSup_eq_Max)
-
-proposition is_interval_compact:
- "is_interval S \<and> compact S \<longleftrightarrow> (\<exists>a b. S = cbox a b)" (is "?lhs = ?rhs")
-proof (cases "S = {}")
- case True
- with empty_as_interval show ?thesis by auto
-next
- case False
- show ?thesis
- proof
- assume L: ?lhs
- then have "is_interval S" "compact S" by auto
- define a where "a \<equiv> \<Sum>i\<in>Basis. (INF x\<in>S. x \<bullet> i) *\<^sub>R i"
- define b where "b \<equiv> \<Sum>i\<in>Basis. (SUP x\<in>S. x \<bullet> i) *\<^sub>R i"
- have 1: "\<And>x i. \<lbrakk>x \<in> S; i \<in> Basis\<rbrakk> \<Longrightarrow> (INF x\<in>S. x \<bullet> i) \<le> x \<bullet> i"
- by (simp add: cInf_lower bounded_inner_imp_bdd_below compact_imp_bounded L)
- have 2: "\<And>x i. \<lbrakk>x \<in> S; i \<in> Basis\<rbrakk> \<Longrightarrow> x \<bullet> i \<le> (SUP x\<in>S. x \<bullet> i)"
- by (simp add: cSup_upper bounded_inner_imp_bdd_above compact_imp_bounded L)
- have 3: "x \<in> S" if inf: "\<And>i. i \<in> Basis \<Longrightarrow> (INF x\<in>S. x \<bullet> i) \<le> x \<bullet> i"
- and sup: "\<And>i. i \<in> Basis \<Longrightarrow> x \<bullet> i \<le> (SUP x\<in>S. x \<bullet> i)" for x
- proof (rule mem_box_componentwiseI [OF \<open>is_interval S\<close>])
- fix i::'a
- assume i: "i \<in> Basis"
- have cont: "continuous_on S (\<lambda>x. x \<bullet> i)"
- by (intro continuous_intros)
- obtain a where "a \<in> S" and a: "\<And>y. y\<in>S \<Longrightarrow> a \<bullet> i \<le> y \<bullet> i"
- using continuous_attains_inf [OF \<open>compact S\<close> False cont] by blast
- obtain b where "b \<in> S" and b: "\<And>y. y\<in>S \<Longrightarrow> y \<bullet> i \<le> b \<bullet> i"
- using continuous_attains_sup [OF \<open>compact S\<close> False cont] by blast
- have "a \<bullet> i \<le> (INF x\<in>S. x \<bullet> i)"
- by (simp add: False a cINF_greatest)
- also have "\<dots> \<le> x \<bullet> i"
- by (simp add: i inf)
- finally have ai: "a \<bullet> i \<le> x \<bullet> i" .
- have "x \<bullet> i \<le> (SUP x\<in>S. x \<bullet> i)"
- by (simp add: i sup)
- also have "(SUP x\<in>S. x \<bullet> i) \<le> b \<bullet> i"
- by (simp add: False b cSUP_least)
- finally have bi: "x \<bullet> i \<le> b \<bullet> i" .
- show "x \<bullet> i \<in> (\<lambda>x. x \<bullet> i) ` S"
- apply (rule_tac x="\<Sum>j\<in>Basis. (if j = i then x \<bullet> i else a \<bullet> j) *\<^sub>R j" in image_eqI)
- apply (simp add: i)
- apply (rule mem_is_intervalI [OF \<open>is_interval S\<close> \<open>a \<in> S\<close> \<open>b \<in> S\<close>])
- using i ai bi apply force
- done
- qed
- have "S = cbox a b"
- by (auto simp: a_def b_def mem_box intro: 1 2 3)
- then show ?rhs
- by blast
- next
- assume R: ?rhs
- then show ?lhs
- using compact_cbox is_interval_cbox by blast
- qed
-qed
-
-text \<open>Hence some handy theorems on distance, diameter etc. of/from a set.\<close>
-
-lemma distance_attains_sup:
- assumes "compact s" "s \<noteq> {}"
- shows "\<exists>x\<in>s. \<forall>y\<in>s. dist a y \<le> dist a x"
-proof (rule continuous_attains_sup [OF assms])
- {
- fix x
- assume "x\<in>s"
- have "(dist a \<longlongrightarrow> dist a x) (at x within s)"
- by (intro tendsto_dist tendsto_const tendsto_ident_at)
- }
- then show "continuous_on s (dist a)"
- unfolding continuous_on ..
-qed
-
-text \<open>For \emph{minimal} distance, we only need closure, not compactness.\<close>
-
-lemma distance_attains_inf:
- fixes a :: "'a::heine_borel"
- assumes "closed s" and "s \<noteq> {}"
- obtains x where "x\<in>s" "\<And>y. y \<in> s \<Longrightarrow> dist a x \<le> dist a y"
-proof -
- from assms obtain b where "b \<in> s" by auto
- let ?B = "s \<inter> cball a (dist b a)"
- have "?B \<noteq> {}" using \<open>b \<in> s\<close>
- by (auto simp: dist_commute)
- moreover have "continuous_on ?B (dist a)"
- by (auto intro!: continuous_at_imp_continuous_on continuous_dist continuous_ident continuous_const)
- moreover have "compact ?B"
- by (intro closed_Int_compact \<open>closed s\<close> compact_cball)
- ultimately obtain x where "x \<in> ?B" "\<forall>y\<in>?B. dist a x \<le> dist a y"
- by (metis continuous_attains_inf)
- with that show ?thesis by fastforce
-qed
-
-
-subsection%unimportant\<open>Relations among convergence and absolute convergence for power series\<close>
-
-lemma summable_imp_bounded:
- fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
- shows "summable f \<Longrightarrow> bounded (range f)"
-by (frule summable_LIMSEQ_zero) (simp add: convergent_imp_bounded)
-
-lemma summable_imp_sums_bounded:
- "summable f \<Longrightarrow> bounded (range (\<lambda>n. sum f {..<n}))"
-by (auto simp: summable_def sums_def dest: convergent_imp_bounded)
-
-lemma power_series_conv_imp_absconv_weak:
- fixes a:: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}" and w :: 'a
- assumes sum: "summable (\<lambda>n. a n * z ^ n)" and no: "norm w < norm z"
- shows "summable (\<lambda>n. of_real(norm(a n)) * w ^ n)"
-proof -
- obtain M where M: "\<And>x. norm (a x * z ^ x) \<le> M"
- using summable_imp_bounded [OF sum] by (force simp: bounded_iff)
- then have *: "summable (\<lambda>n. norm (a n) * norm w ^ n)"
- by (rule_tac M=M in Abel_lemma) (auto simp: norm_mult norm_power intro: no)
- show ?thesis
- apply (rule series_comparison_complex [of "(\<lambda>n. of_real(norm(a n) * norm w ^ n))"])
- apply (simp only: summable_complex_of_real *)
- apply (auto simp: norm_mult norm_power)
- done
-qed
-
-subsection%unimportant \<open>Bounded closed nest property (proof does not use Heine-Borel)\<close>
-
-lemma bounded_closed_nest:
- fixes S :: "nat \<Rightarrow> ('a::heine_borel) set"
- assumes "\<And>n. closed (S n)"
- and "\<And>n. S n \<noteq> {}"
- and "\<And>m n. m \<le> n \<Longrightarrow> S n \<subseteq> S m"
- and "bounded (S 0)"
- obtains a where "\<And>n. a \<in> S n"
-proof -
- from assms(2) obtain x where x: "\<forall>n. x n \<in> S n"
- using choice[of "\<lambda>n x. x \<in> S n"] by auto
- from assms(4,1) have "seq_compact (S 0)"
- by (simp add: bounded_closed_imp_seq_compact)
- then obtain l r where lr: "l \<in> S 0" "strict_mono r" "(x \<circ> r) \<longlonglongrightarrow> l"
- using x and assms(3) unfolding seq_compact_def by blast
- have "\<forall>n. l \<in> S n"
- proof
- fix n :: nat
- have "closed (S n)"
- using assms(1) by simp
- moreover have "\<forall>i. (x \<circ> r) i \<in> S i"
- using x and assms(3) and lr(2) [THEN seq_suble] by auto
- then have "\<forall>i. (x \<circ> r) (i + n) \<in> S n"
- using assms(3) by (fast intro!: le_add2)
- moreover have "(\<lambda>i. (x \<circ> r) (i + n)) \<longlonglongrightarrow> l"
- using lr(3) by (rule LIMSEQ_ignore_initial_segment)
- ultimately show "l \<in> S n"
- by (rule closed_sequentially)
- qed
- then show ?thesis
- using that by blast
-qed
-
-text \<open>Decreasing case does not even need compactness, just completeness.\<close>
-
-lemma decreasing_closed_nest:
- fixes S :: "nat \<Rightarrow> ('a::complete_space) set"
- assumes "\<And>n. closed (S n)"
- "\<And>n. S n \<noteq> {}"
- "\<And>m n. m \<le> n \<Longrightarrow> S n \<subseteq> S m"
- "\<And>e. e>0 \<Longrightarrow> \<exists>n. \<forall>x\<in>S n. \<forall>y\<in>S n. dist x y < e"
- obtains a where "\<And>n. a \<in> S n"
-proof -
- have "\<forall>n. \<exists>x. x \<in> S n"
- using assms(2) by auto
- then have "\<exists>t. \<forall>n. t n \<in> S n"
- using choice[of "\<lambda>n x. x \<in> S n"] by auto
- then obtain t where t: "\<forall>n. t n \<in> S n" by auto
- {
- fix e :: real
- assume "e > 0"
- then obtain N where N: "\<forall>x\<in>S N. \<forall>y\<in>S N. dist x y < e"
- using assms(4) by blast
- {
- fix m n :: nat
- assume "N \<le> m \<and> N \<le> n"
- then have "t m \<in> S N" "t n \<in> S N"
- using assms(3) t unfolding subset_eq t by blast+
- then have "dist (t m) (t n) < e"
- using N by auto
- }
- then have "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (t m) (t n) < e"
- by auto
- }
- then have "Cauchy t"
- unfolding cauchy_def by auto
- then obtain l where l:"(t \<longlongrightarrow> l) sequentially"
- using complete_UNIV unfolding complete_def by auto
- { fix n :: nat
- { fix e :: real
- assume "e > 0"
- then obtain N :: nat where N: "\<forall>n\<ge>N. dist (t n) l < e"
- using l[unfolded lim_sequentially] by auto
- have "t (max n N) \<in> S n"
- by (meson assms(3) contra_subsetD max.cobounded1 t)
- then have "\<exists>y\<in>S n. dist y l < e"
- using N max.cobounded2 by blast
- }
- then have "l \<in> S n"
- using closed_approachable[of "S n" l] assms(1) by auto
- }
- then show ?thesis
- using that by blast
-qed
-
-text \<open>Strengthen it to the intersection actually being a singleton.\<close>
-
-lemma decreasing_closed_nest_sing:
- fixes S :: "nat \<Rightarrow> 'a::complete_space set"
- assumes "\<And>n. closed(S n)"
- "\<And>n. S n \<noteq> {}"
- "\<And>m n. m \<le> n \<Longrightarrow> S n \<subseteq> S m"
- "\<And>e. e>0 \<Longrightarrow> \<exists>n. \<forall>x \<in> (S n). \<forall> y\<in>(S n). dist x y < e"
- shows "\<exists>a. \<Inter>(range S) = {a}"
-proof -
- obtain a where a: "\<forall>n. a \<in> S n"
- using decreasing_closed_nest[of S] using assms by auto
- { fix b
- assume b: "b \<in> \<Inter>(range S)"
- { fix e :: real
- assume "e > 0"
- then have "dist a b < e"
- using assms(4) and b and a by blast
- }
- then have "dist a b = 0"
- by (metis dist_eq_0_iff dist_nz less_le)
- }
- with a have "\<Inter>(range S) = {a}"
- unfolding image_def by auto
- then show ?thesis ..
-qed
-
-
-subsection \<open>Infimum Distance\<close>
-
-definition%important "infdist x A = (if A = {} then 0 else INF a\<in>A. dist x a)"
-
-lemma bdd_below_image_dist[intro, simp]: "bdd_below (dist x ` A)"
- by (auto intro!: zero_le_dist)
-
-lemma infdist_notempty: "A \<noteq> {} \<Longrightarrow> infdist x A = (INF a\<in>A. dist x a)"
- by (simp add: infdist_def)
-
-lemma infdist_nonneg: "0 \<le> infdist x A"
- by (auto simp: infdist_def intro: cINF_greatest)
-
-lemma infdist_le: "a \<in> A \<Longrightarrow> infdist x A \<le> dist x a"
- by (auto intro: cINF_lower simp add: infdist_def)
-
-lemma infdist_le2: "a \<in> A \<Longrightarrow> dist x a \<le> d \<Longrightarrow> infdist x A \<le> d"
- by (auto intro!: cINF_lower2 simp add: infdist_def)
-
-lemma infdist_zero[simp]: "a \<in> A \<Longrightarrow> infdist a A = 0"
- by (auto intro!: antisym infdist_nonneg infdist_le2)
-
-lemma infdist_triangle: "infdist x A \<le> infdist y A + dist x y"
-proof (cases "A = {}")
- case True
- then show ?thesis by (simp add: infdist_def)
-next
- case False
- then obtain a where "a \<in> A" by auto
- have "infdist x A \<le> Inf {dist x y + dist y a |a. a \<in> A}"
- proof (rule cInf_greatest)
- from \<open>A \<noteq> {}\<close> show "{dist x y + dist y a |a. a \<in> A} \<noteq> {}"
- by simp
- fix d
- assume "d \<in> {dist x y + dist y a |a. a \<in> A}"
- then obtain a where d: "d = dist x y + dist y a" "a \<in> A"
- by auto
- show "infdist x A \<le> d"
- unfolding infdist_notempty[OF \<open>A \<noteq> {}\<close>]
- proof (rule cINF_lower2)
- show "a \<in> A" by fact
- show "dist x a \<le> d"
- unfolding d by (rule dist_triangle)
- qed simp
- qed
- also have "\<dots> = dist x y + infdist y A"
- proof (rule cInf_eq, safe)
- fix a
- assume "a \<in> A"
- then show "dist x y + infdist y A \<le> dist x y + dist y a"
- by (auto intro: infdist_le)
- next
- fix i
- assume inf: "\<And>d. d \<in> {dist x y + dist y a |a. a \<in> A} \<Longrightarrow> i \<le> d"
- then have "i - dist x y \<le> infdist y A"
- unfolding infdist_notempty[OF \<open>A \<noteq> {}\<close>] using \<open>a \<in> A\<close>
- by (intro cINF_greatest) (auto simp: field_simps)
- then show "i \<le> dist x y + infdist y A"
- by simp
- qed
- finally show ?thesis by simp
-qed
-
-lemma in_closure_iff_infdist_zero:
- assumes "A \<noteq> {}"
- shows "x \<in> closure A \<longleftrightarrow> infdist x A = 0"
-proof
- assume "x \<in> closure A"
- show "infdist x A = 0"
- proof (rule ccontr)
- assume "infdist x A \<noteq> 0"
- with infdist_nonneg[of x A] have "infdist x A > 0"
- by auto
- then have "ball x (infdist x A) \<inter> closure A = {}"
- apply auto
- apply (metis \<open>x \<in> closure A\<close> closure_approachable dist_commute infdist_le not_less)
- done
- then have "x \<notin> closure A"
- by (metis \<open>0 < infdist x A\<close> centre_in_ball disjoint_iff_not_equal)
- then show False using \<open>x \<in> closure A\<close> by simp
- qed
-next
- assume x: "infdist x A = 0"
- then obtain a where "a \<in> A"
- by atomize_elim (metis all_not_in_conv assms)
- show "x \<in> closure A"
- unfolding closure_approachable
- apply safe
- proof (rule ccontr)
- fix e :: real
- assume "e > 0"
- assume "\<not> (\<exists>y\<in>A. dist y x < e)"
- then have "infdist x A \<ge> e" using \<open>a \<in> A\<close>
- unfolding infdist_def
- by (force simp: dist_commute intro: cINF_greatest)
- with x \<open>e > 0\<close> show False by auto
- qed
-qed
-
-lemma in_closed_iff_infdist_zero:
- assumes "closed A" "A \<noteq> {}"
- shows "x \<in> A \<longleftrightarrow> infdist x A = 0"
-proof -
- have "x \<in> closure A \<longleftrightarrow> infdist x A = 0"
- by (rule in_closure_iff_infdist_zero) fact
- with assms show ?thesis by simp
-qed
-
-lemma infdist_pos_not_in_closed:
- assumes "closed S" "S \<noteq> {}" "x \<notin> S"
- shows "infdist x S > 0"
-using in_closed_iff_infdist_zero[OF assms(1) assms(2), of x] assms(3) infdist_nonneg le_less by fastforce
-
-lemma
- infdist_attains_inf:
- fixes X::"'a::heine_borel set"
- assumes "closed X"
- assumes "X \<noteq> {}"
- obtains x where "x \<in> X" "infdist y X = dist y x"
-proof -
- have "bdd_below (dist y ` X)"
- by auto
- from distance_attains_inf[OF assms, of y]
- obtain x where INF: "x \<in> X" "\<And>z. z \<in> X \<Longrightarrow> dist y x \<le> dist y z" by auto
- have "infdist y X = dist y x"
- by (auto simp: infdist_def assms
- intro!: antisym cINF_lower[OF _ \<open>x \<in> X\<close>] cINF_greatest[OF assms(2) INF(2)])
- with \<open>x \<in> X\<close> show ?thesis ..
-qed
-
-
-text \<open>Every metric space is a T4 space:\<close>
-
-instance metric_space \<subseteq> t4_space
-proof
- fix S T::"'a set" assume H: "closed S" "closed T" "S \<inter> T = {}"
- consider "S = {}" | "T = {}" | "S \<noteq> {} \<and> T \<noteq> {}" by auto
- then show "\<exists>U V. open U \<and> open V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> U \<inter> V = {}"
- proof (cases)
- case 1
- show ?thesis
- apply (rule exI[of _ "{}"], rule exI[of _ UNIV]) using 1 by auto
- next
- case 2
- show ?thesis
- apply (rule exI[of _ UNIV], rule exI[of _ "{}"]) using 2 by auto
- next
- case 3
- define U where "U = (\<Union>x\<in>S. ball x ((infdist x T)/2))"
- have A: "open U" unfolding U_def by auto
- have "infdist x T > 0" if "x \<in> S" for x
- using H that 3 by (auto intro!: infdist_pos_not_in_closed)
- then have B: "S \<subseteq> U" unfolding U_def by auto
- define V where "V = (\<Union>x\<in>T. ball x ((infdist x S)/2))"
- have C: "open V" unfolding V_def by auto
- have "infdist x S > 0" if "x \<in> T" for x
- using H that 3 by (auto intro!: infdist_pos_not_in_closed)
- then have D: "T \<subseteq> V" unfolding V_def by auto
-
- have "(ball x ((infdist x T)/2)) \<inter> (ball y ((infdist y S)/2)) = {}" if "x \<in> S" "y \<in> T" for x y
- proof (auto)
- fix z assume H: "dist x z * 2 < infdist x T" "dist y z * 2 < infdist y S"
- have "2 * dist x y \<le> 2 * dist x z + 2 * dist y z"
- using dist_triangle[of x y z] by (auto simp add: dist_commute)
- also have "... < infdist x T + infdist y S"
- using H by auto
- finally have "dist x y < infdist x T \<or> dist x y < infdist y S"
- by auto
- then show False
- using infdist_le[OF \<open>x \<in> S\<close>, of y] infdist_le[OF \<open>y \<in> T\<close>, of x] by (auto simp add: dist_commute)
- qed
- then have E: "U \<inter> V = {}"
- unfolding U_def V_def by auto
- show ?thesis
- apply (rule exI[of _ U], rule exI[of _ V]) using A B C D E by auto
- qed
-qed
-
-lemma tendsto_infdist [tendsto_intros]:
- assumes f: "(f \<longlongrightarrow> l) F"
- shows "((\<lambda>x. infdist (f x) A) \<longlongrightarrow> infdist l A) F"
-proof (rule tendstoI)
- fix e ::real
- assume "e > 0"
- from tendstoD[OF f this]
- show "eventually (\<lambda>x. dist (infdist (f x) A) (infdist l A) < e) F"
- proof (eventually_elim)
- fix x
- from infdist_triangle[of l A "f x"] infdist_triangle[of "f x" A l]
- have "dist (infdist (f x) A) (infdist l A) \<le> dist (f x) l"
- by (simp add: dist_commute dist_real_def)
- also assume "dist (f x) l < e"
- finally show "dist (infdist (f x) A) (infdist l A) < e" .
- qed
-qed
-
-lemma continuous_infdist[continuous_intros]:
- assumes "continuous F f"
- shows "continuous F (\<lambda>x. infdist (f x) A)"
- using assms unfolding continuous_def by (rule tendsto_infdist)
-
-lemma compact_infdist_le:
- fixes A::"'a::heine_borel set"
- assumes "A \<noteq> {}"
- assumes "compact A"
- assumes "e > 0"
- shows "compact {x. infdist x A \<le> e}"
-proof -
- from continuous_closed_vimage[of "{0..e}" "\<lambda>x. infdist x A"]
- continuous_infdist[OF continuous_ident, of _ UNIV A]
- have "closed {x. infdist x A \<le> e}" by (auto simp: vimage_def infdist_nonneg)
- moreover
- from assms obtain x0 b where b: "\<And>x. x \<in> A \<Longrightarrow> dist x0 x \<le> b" "closed A"
- by (auto simp: compact_eq_bounded_closed bounded_def)
- {
- fix y
- assume le: "infdist y A \<le> e"
- from infdist_attains_inf[OF \<open>closed A\<close> \<open>A \<noteq> {}\<close>, of y]
- obtain z where z: "z \<in> A" "infdist y A = dist y z" by blast
- have "dist x0 y \<le> dist y z + dist x0 z"
- by (metis dist_commute dist_triangle)
- also have "dist y z \<le> e" using le z by simp
- also have "dist x0 z \<le> b" using b z by simp
- finally have "dist x0 y \<le> b + e" by arith
- } then
- have "bounded {x. infdist x A \<le> e}"
- by (auto simp: bounded_any_center[where a=x0] intro!: exI[where x="b + e"])
- ultimately show "compact {x. infdist x A \<le> e}"
- by (simp add: compact_eq_bounded_closed)
-qed
-
-subsection%unimportant \<open>Equality of continuous functions on closure and related results\<close>
-
-lemma continuous_closedin_preimage_constant:
- fixes f :: "_ \<Rightarrow> 'b::t1_space"
- shows "continuous_on S f \<Longrightarrow> closedin (subtopology euclidean S) {x \<in> S. f x = a}"
- using continuous_closedin_preimage[of S f "{a}"] by (simp add: vimage_def Collect_conj_eq)
-
-lemma continuous_closed_preimage_constant:
- fixes f :: "_ \<Rightarrow> 'b::t1_space"
- shows "continuous_on S f \<Longrightarrow> closed S \<Longrightarrow> closed {x \<in> S. f x = a}"
- using continuous_closed_preimage[of S f "{a}"] by (simp add: vimage_def Collect_conj_eq)
-
-lemma continuous_constant_on_closure:
- fixes f :: "_ \<Rightarrow> 'b::t1_space"
- assumes "continuous_on (closure S) f"
- and "\<And>x. x \<in> S \<Longrightarrow> f x = a"
- and "x \<in> closure S"
- shows "f x = a"
- using continuous_closed_preimage_constant[of "closure S" f a]
- assms closure_minimal[of S "{x \<in> closure S. f x = a}"] closure_subset
- unfolding subset_eq
- by auto
-
-lemma image_closure_subset:
- assumes contf: "continuous_on (closure S) f"
- and "closed T"
- and "(f ` S) \<subseteq> T"
- shows "f ` (closure S) \<subseteq> T"
-proof -
- have "S \<subseteq> {x \<in> closure S. f x \<in> T}"
- using assms(3) closure_subset by auto
- moreover have "closed (closure S \<inter> f -` T)"
- using continuous_closed_preimage[OF contf] \<open>closed T\<close> by auto
- ultimately have "closure S = (closure S \<inter> f -` T)"
- using closure_minimal[of S "(closure S \<inter> f -` T)"] by auto
- then show ?thesis by auto
-qed
-
-lemma continuous_on_closure_norm_le:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
- assumes "continuous_on (closure s) f"
- and "\<forall>y \<in> s. norm(f y) \<le> b"
- and "x \<in> (closure s)"
- shows "norm (f x) \<le> b"
-proof -
- have *: "f ` s \<subseteq> cball 0 b"
- using assms(2)[unfolded mem_cball_0[symmetric]] by auto
- show ?thesis
- by (meson "*" assms(1) assms(3) closed_cball image_closure_subset image_subset_iff mem_cball_0)
-qed
-
-lemma isCont_indicator:
- fixes x :: "'a::t2_space"
- shows "isCont (indicator A :: 'a \<Rightarrow> real) x = (x \<notin> frontier A)"
-proof auto
- fix x
- assume cts_at: "isCont (indicator A :: 'a \<Rightarrow> real) x" and fr: "x \<in> frontier A"
- with continuous_at_open have 1: "\<forall>V::real set. open V \<and> indicator A x \<in> V \<longrightarrow>
- (\<exists>U::'a set. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> V))" by auto
- show False
- proof (cases "x \<in> A")
- assume x: "x \<in> A"
- hence "indicator A x \<in> ({0<..<2} :: real set)" by simp
- hence "\<exists>U. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> ({0<..<2} :: real set))"
- using 1 open_greaterThanLessThan by blast
- then guess U .. note U = this
- hence "\<forall>y\<in>U. indicator A y > (0::real)"
- unfolding greaterThanLessThan_def by auto
- hence "U \<subseteq> A" using indicator_eq_0_iff by force
- hence "x \<in> interior A" using U interiorI by auto
- thus ?thesis using fr unfolding frontier_def by simp
- next
- assume x: "x \<notin> A"
- hence "indicator A x \<in> ({-1<..<1} :: real set)" by simp
- hence "\<exists>U. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> ({-1<..<1} :: real set))"
- using 1 open_greaterThanLessThan by blast
- then guess U .. note U = this
- hence "\<forall>y\<in>U. indicator A y < (1::real)"
- unfolding greaterThanLessThan_def by auto
- hence "U \<subseteq> -A" by auto
- hence "x \<in> interior (-A)" using U interiorI by auto
- thus ?thesis using fr interior_complement unfolding frontier_def by auto
- qed
-next
- assume nfr: "x \<notin> frontier A"
- hence "x \<in> interior A \<or> x \<in> interior (-A)"
- by (auto simp: frontier_def closure_interior)
- thus "isCont ((indicator A)::'a \<Rightarrow> real) x"
- proof
- assume int: "x \<in> interior A"
- then obtain U where U: "open U" "x \<in> U" "U \<subseteq> A" unfolding interior_def by auto
- hence "\<forall>y\<in>U. indicator A y = (1::real)" unfolding indicator_def by auto
- hence "continuous_on U (indicator A)" by (simp add: continuous_on_const indicator_eq_1_iff)
- thus ?thesis using U continuous_on_eq_continuous_at by auto
- next
- assume ext: "x \<in> interior (-A)"
- then obtain U where U: "open U" "x \<in> U" "U \<subseteq> -A" unfolding interior_def by auto
- then have "continuous_on U (indicator A)"
- using continuous_on_topological by (auto simp: subset_iff)
- thus ?thesis using U continuous_on_eq_continuous_at by auto
- qed
-qed
-
-subsection%unimportant \<open>A function constant on a set\<close>
-
-definition constant_on (infixl "(constant'_on)" 50)
- where "f constant_on A \<equiv> \<exists>y. \<forall>x\<in>A. f x = y"
-
-lemma constant_on_subset: "\<lbrakk>f constant_on A; B \<subseteq> A\<rbrakk> \<Longrightarrow> f constant_on B"
- unfolding constant_on_def by blast
-
-lemma injective_not_constant:
- fixes S :: "'a::{perfect_space} set"
- shows "\<lbrakk>open S; inj_on f S; f constant_on S\<rbrakk> \<Longrightarrow> S = {}"
-unfolding constant_on_def
-by (metis equals0I inj_on_contraD islimpt_UNIV islimpt_def)
-
-lemma constant_on_closureI:
- fixes f :: "_ \<Rightarrow> 'b::t1_space"
- assumes cof: "f constant_on S" and contf: "continuous_on (closure S) f"
- shows "f constant_on (closure S)"
-using continuous_constant_on_closure [OF contf] cof unfolding constant_on_def
-by metis
-
-subsection%unimportant\<open>Relating linear images to open/closed/interior/closure\<close>
-
-proposition open_surjective_linear_image:
- fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
- assumes "open A" "linear f" "surj f"
- shows "open(f ` A)"
-unfolding open_dist
-proof clarify
- fix x
- assume "x \<in> A"
- have "bounded (inv f ` Basis)"
- by (simp add: finite_imp_bounded)
- with bounded_pos obtain B where "B > 0" and B: "\<And>x. x \<in> inv f ` Basis \<Longrightarrow> norm x \<le> B"
- by metis
- obtain e where "e > 0" and e: "\<And>z. dist z x < e \<Longrightarrow> z \<in> A"
- by (metis open_dist \<open>x \<in> A\<close> \<open>open A\<close>)
- define \<delta> where "\<delta> \<equiv> e / B / DIM('b)"
- show "\<exists>e>0. \<forall>y. dist y (f x) < e \<longrightarrow> y \<in> f ` A"
- proof (intro exI conjI)
- show "\<delta> > 0"
- using \<open>e > 0\<close> \<open>B > 0\<close> by (simp add: \<delta>_def divide_simps)
- have "y \<in> f ` A" if "dist y (f x) * (B * real DIM('b)) < e" for y
- proof -
- define u where "u \<equiv> y - f x"
- show ?thesis
- proof (rule image_eqI)
- show "y = f (x + (\<Sum>i\<in>Basis. (u \<bullet> i) *\<^sub>R inv f i))"
- apply (simp add: linear_add linear_sum linear.scaleR \<open>linear f\<close> surj_f_inv_f \<open>surj f\<close>)
- apply (simp add: euclidean_representation u_def)
- done
- have "dist (x + (\<Sum>i\<in>Basis. (u \<bullet> i) *\<^sub>R inv f i)) x \<le> (\<Sum>i\<in>Basis. norm ((u \<bullet> i) *\<^sub>R inv f i))"
- by (simp add: dist_norm sum_norm_le)
- also have "... = (\<Sum>i\<in>Basis. \<bar>u \<bullet> i\<bar> * norm (inv f i))"
- by simp
- also have "... \<le> (\<Sum>i\<in>Basis. \<bar>u \<bullet> i\<bar>) * B"
- by (simp add: B sum_distrib_right sum_mono mult_left_mono)
- also have "... \<le> DIM('b) * dist y (f x) * B"
- apply (rule mult_right_mono [OF sum_bounded_above])
- using \<open>0 < B\<close> by (auto simp: Basis_le_norm dist_norm u_def)
- also have "... < e"
- by (metis mult.commute mult.left_commute that)
- finally show "x + (\<Sum>i\<in>Basis. (u \<bullet> i) *\<^sub>R inv f i) \<in> A"
- by (rule e)
- qed
- qed
- then show "\<forall>y. dist y (f x) < \<delta> \<longrightarrow> y \<in> f ` A"
- using \<open>e > 0\<close> \<open>B > 0\<close>
- by (auto simp: \<delta>_def divide_simps mult_less_0_iff)
- qed
-qed
-
-corollary open_bijective_linear_image_eq:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
- assumes "linear f" "bij f"
- shows "open(f ` A) \<longleftrightarrow> open A"
-proof
- assume "open(f ` A)"
- then have "open(f -` (f ` A))"
- using assms by (force simp: linear_continuous_at linear_conv_bounded_linear continuous_open_vimage)
- then show "open A"
- by (simp add: assms bij_is_inj inj_vimage_image_eq)
-next
- assume "open A"
- then show "open(f ` A)"
- by (simp add: assms bij_is_surj open_surjective_linear_image)
-qed
-
-corollary interior_bijective_linear_image:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
- assumes "linear f" "bij f"
- shows "interior (f ` S) = f ` interior S" (is "?lhs = ?rhs")
-proof safe
- fix x
- assume x: "x \<in> ?lhs"
- then obtain T where "open T" and "x \<in> T" and "T \<subseteq> f ` S"
- by (metis interiorE)
- then show "x \<in> ?rhs"
- by (metis (no_types, hide_lams) assms subsetD interior_maximal open_bijective_linear_image_eq subset_image_iff)
-next
- fix x
- assume x: "x \<in> interior S"
- then show "f x \<in> interior (f ` S)"
- by (meson assms imageI image_mono interiorI interior_subset open_bijective_linear_image_eq open_interior)
-qed
-
-lemma interior_injective_linear_image:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
- assumes "linear f" "inj f"
- shows "interior(f ` S) = f ` (interior S)"
- by (simp add: linear_injective_imp_surjective assms bijI interior_bijective_linear_image)
-
-lemma interior_surjective_linear_image:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
- assumes "linear f" "surj f"
- shows "interior(f ` S) = f ` (interior S)"
- by (simp add: assms interior_injective_linear_image linear_surjective_imp_injective)
-
-lemma interior_negations:
- fixes S :: "'a::euclidean_space set"
- shows "interior(uminus ` S) = image uminus (interior S)"
- by (simp add: bij_uminus interior_bijective_linear_image linear_uminus)
-
-text \<open>Preservation of compactness and connectedness under continuous function.\<close>
-
-lemma compact_eq_openin_cover:
- "compact S \<longleftrightarrow>
- (\<forall>C. (\<forall>c\<in>C. openin (subtopology euclidean S) c) \<and> S \<subseteq> \<Union>C \<longrightarrow>
- (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D))"
-proof safe
- fix C
- assume "compact S" and "\<forall>c\<in>C. openin (subtopology euclidean S) c" and "S \<subseteq> \<Union>C"
- then have "\<forall>c\<in>{T. open T \<and> S \<inter> T \<in> C}. open c" and "S \<subseteq> \<Union>{T. open T \<and> S \<inter> T \<in> C}"
- unfolding openin_open by force+
- with \<open>compact S\<close> obtain D where "D \<subseteq> {T. open T \<and> S \<inter> T \<in> C}" and "finite D" and "S \<subseteq> \<Union>D"
- by (meson compactE)
- then have "image (\<lambda>T. S \<inter> T) D \<subseteq> C \<and> finite (image (\<lambda>T. S \<inter> T) D) \<and> S \<subseteq> \<Union>(image (\<lambda>T. S \<inter> T) D)"
- by auto
- then show "\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D" ..
-next
- assume 1: "\<forall>C. (\<forall>c\<in>C. openin (subtopology euclidean S) c) \<and> S \<subseteq> \<Union>C \<longrightarrow>
- (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D)"
- show "compact S"
- proof (rule compactI)
- fix C
- let ?C = "image (\<lambda>T. S \<inter> T) C"
- assume "\<forall>t\<in>C. open t" and "S \<subseteq> \<Union>C"
- then have "(\<forall>c\<in>?C. openin (subtopology euclidean S) c) \<and> S \<subseteq> \<Union>?C"
- unfolding openin_open by auto
- with 1 obtain D where "D \<subseteq> ?C" and "finite D" and "S \<subseteq> \<Union>D"
- by metis
- let ?D = "inv_into C (\<lambda>T. S \<inter> T) ` D"
- have "?D \<subseteq> C \<and> finite ?D \<and> S \<subseteq> \<Union>?D"
- proof (intro conjI)
- from \<open>D \<subseteq> ?C\<close> show "?D \<subseteq> C"
- by (fast intro: inv_into_into)
- from \<open>finite D\<close> show "finite ?D"
- by (rule finite_imageI)
- from \<open>S \<subseteq> \<Union>D\<close> show "S \<subseteq> \<Union>?D"
- apply (rule subset_trans, clarsimp)
- apply (frule subsetD [OF \<open>D \<subseteq> ?C\<close>, THEN f_inv_into_f])
- apply (erule rev_bexI, fast)
- done
- qed
- then show "\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D" ..
- qed
-qed
-
-subsection%unimportant\<open> Theorems relating continuity and uniform continuity to closures\<close>
-
-lemma continuous_on_closure:
- "continuous_on (closure S) f \<longleftrightarrow>
- (\<forall>x e. x \<in> closure S \<and> 0 < e
- \<longrightarrow> (\<exists>d. 0 < d \<and> (\<forall>y. y \<in> S \<and> dist y x < d \<longrightarrow> dist (f y) (f x) < e)))"
- (is "?lhs = ?rhs")
-proof
- assume ?lhs then show ?rhs
- unfolding continuous_on_iff by (metis Un_iff closure_def)
-next
- assume R [rule_format]: ?rhs
- show ?lhs
- proof
- fix x and e::real
- assume "0 < e" and x: "x \<in> closure S"
- obtain \<delta>::real where "\<delta> > 0"
- and \<delta>: "\<And>y. \<lbrakk>y \<in> S; dist y x < \<delta>\<rbrakk> \<Longrightarrow> dist (f y) (f x) < e/2"
- using R [of x "e/2"] \<open>0 < e\<close> x by auto
- have "dist (f y) (f x) \<le> e" if y: "y \<in> closure S" and dyx: "dist y x < \<delta>/2" for y
- proof -
- obtain \<delta>'::real where "\<delta>' > 0"
- and \<delta>': "\<And>z. \<lbrakk>z \<in> S; dist z y < \<delta>'\<rbrakk> \<Longrightarrow> dist (f z) (f y) < e/2"
- using R [of y "e/2"] \<open>0 < e\<close> y by auto
- obtain z where "z \<in> S" and z: "dist z y < min \<delta>' \<delta> / 2"
- using closure_approachable y
- by (metis \<open>0 < \<delta>'\<close> \<open>0 < \<delta>\<close> divide_pos_pos min_less_iff_conj zero_less_numeral)
- have "dist (f z) (f y) < e/2"
- apply (rule \<delta>' [OF \<open>z \<in> S\<close>])
- using z \<open>0 < \<delta>'\<close> by linarith
- moreover have "dist (f z) (f x) < e/2"
- apply (rule \<delta> [OF \<open>z \<in> S\<close>])
- using z \<open>0 < \<delta>\<close> dist_commute[of y z] dist_triangle_half_r [of y] dyx by auto
- ultimately show ?thesis
- by (metis dist_commute dist_triangle_half_l less_imp_le)
- qed
- then show "\<exists>d>0. \<forall>x'\<in>closure S. dist x' x < d \<longrightarrow> dist (f x') (f x) \<le> e"
- by (rule_tac x="\<delta>/2" in exI) (simp add: \<open>\<delta> > 0\<close>)
- qed
-qed
-
-lemma continuous_on_closure_sequentially:
- fixes f :: "'a::metric_space \<Rightarrow> 'b :: metric_space"
- shows
- "continuous_on (closure S) f \<longleftrightarrow>
- (\<forall>x a. a \<in> closure S \<and> (\<forall>n. x n \<in> S) \<and> x \<longlonglongrightarrow> a \<longrightarrow> (f \<circ> x) \<longlonglongrightarrow> f a)"
- (is "?lhs = ?rhs")
-proof -
- have "continuous_on (closure S) f \<longleftrightarrow>
- (\<forall>x \<in> closure S. continuous (at x within S) f)"
- by (force simp: continuous_on_closure continuous_within_eps_delta)
- also have "... = ?rhs"
- by (force simp: continuous_within_sequentially)
- finally show ?thesis .
-qed
-
-lemma uniformly_continuous_on_closure:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
- assumes ucont: "uniformly_continuous_on S f"
- and cont: "continuous_on (closure S) f"
- shows "uniformly_continuous_on (closure S) f"
-unfolding uniformly_continuous_on_def
-proof (intro allI impI)
- fix e::real
- assume "0 < e"
- then obtain d::real
- where "d>0"
- and d: "\<And>x x'. \<lbrakk>x\<in>S; x'\<in>S; dist x' x < d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e/3"
- using ucont [unfolded uniformly_continuous_on_def, rule_format, of "e/3"] by auto
- show "\<exists>d>0. \<forall>x\<in>closure S. \<forall>x'\<in>closure S. dist x' x < d \<longrightarrow> dist (f x') (f x) < e"
- proof (rule exI [where x="d/3"], clarsimp simp: \<open>d > 0\<close>)
- fix x y
- assume x: "x \<in> closure S" and y: "y \<in> closure S" and dyx: "dist y x * 3 < d"
- obtain d1::real where "d1 > 0"
- and d1: "\<And>w. \<lbrakk>w \<in> closure S; dist w x < d1\<rbrakk> \<Longrightarrow> dist (f w) (f x) < e/3"
- using cont [unfolded continuous_on_iff, rule_format, of "x" "e/3"] \<open>0 < e\<close> x by auto
- obtain x' where "x' \<in> S" and x': "dist x' x < min d1 (d / 3)"
- using closure_approachable [of x S]
- by (metis \<open>0 < d1\<close> \<open>0 < d\<close> divide_pos_pos min_less_iff_conj x zero_less_numeral)
- obtain d2::real where "d2 > 0"
- and d2: "\<forall>w \<in> closure S. dist w y < d2 \<longrightarrow> dist (f w) (f y) < e/3"
- using cont [unfolded continuous_on_iff, rule_format, of "y" "e/3"] \<open>0 < e\<close> y by auto
- obtain y' where "y' \<in> S" and y': "dist y' y < min d2 (d / 3)"
- using closure_approachable [of y S]
- by (metis \<open>0 < d2\<close> \<open>0 < d\<close> divide_pos_pos min_less_iff_conj y zero_less_numeral)
- have "dist x' x < d/3" using x' by auto
- moreover have "dist x y < d/3"
- by (metis dist_commute dyx less_divide_eq_numeral1(1))
- moreover have "dist y y' < d/3"
- by (metis (no_types) dist_commute min_less_iff_conj y')
- ultimately have "dist x' y' < d/3 + d/3 + d/3"
- by (meson dist_commute_lessI dist_triangle_lt add_strict_mono)
- then have "dist x' y' < d" by simp
- then have "dist (f x') (f y') < e/3"
- by (rule d [OF \<open>y' \<in> S\<close> \<open>x' \<in> S\<close>])
- moreover have "dist (f x') (f x) < e/3" using \<open>x' \<in> S\<close> closure_subset x' d1
- by (simp add: closure_def)
- moreover have "dist (f y') (f y) < e/3" using \<open>y' \<in> S\<close> closure_subset y' d2
- by (simp add: closure_def)
- ultimately have "dist (f y) (f x) < e/3 + e/3 + e/3"
- by (meson dist_commute_lessI dist_triangle_lt add_strict_mono)
- then show "dist (f y) (f x) < e" by simp
- qed
-qed
-
-lemma uniformly_continuous_on_extension_at_closure:
- fixes f::"'a::metric_space \<Rightarrow> 'b::complete_space"
- assumes uc: "uniformly_continuous_on X f"
- assumes "x \<in> closure X"
- obtains l where "(f \<longlongrightarrow> l) (at x within X)"
-proof -
- from assms obtain xs where xs: "xs \<longlonglongrightarrow> x" "\<And>n. xs n \<in> X"
- by (auto simp: closure_sequential)
-
- from uniformly_continuous_on_Cauchy[OF uc LIMSEQ_imp_Cauchy, OF xs]
- obtain l where l: "(\<lambda>n. f (xs n)) \<longlonglongrightarrow> l"
- by atomize_elim (simp only: convergent_eq_Cauchy)
-
- have "(f \<longlongrightarrow> l) (at x within X)"
- proof (safe intro!: Lim_within_LIMSEQ)
- fix xs'
- assume "\<forall>n. xs' n \<noteq> x \<and> xs' n \<in> X"
- and xs': "xs' \<longlonglongrightarrow> x"
- then have "xs' n \<noteq> x" "xs' n \<in> X" for n by auto
-
- from uniformly_continuous_on_Cauchy[OF uc LIMSEQ_imp_Cauchy, OF \<open>xs' \<longlonglongrightarrow> x\<close> \<open>xs' _ \<in> X\<close>]
- obtain l' where l': "(\<lambda>n. f (xs' n)) \<longlonglongrightarrow> l'"
- by atomize_elim (simp only: convergent_eq_Cauchy)
-
- show "(\<lambda>n. f (xs' n)) \<longlonglongrightarrow> l"
- proof (rule tendstoI)
- fix e::real assume "e > 0"
- define e' where "e' \<equiv> e / 2"
- have "e' > 0" using \<open>e > 0\<close> by (simp add: e'_def)
-
- have "\<forall>\<^sub>F n in sequentially. dist (f (xs n)) l < e'"
- by (simp add: \<open>0 < e'\<close> l tendstoD)
- moreover
- from uc[unfolded uniformly_continuous_on_def, rule_format, OF \<open>e' > 0\<close>]
- obtain d where d: "d > 0" "\<And>x x'. x \<in> X \<Longrightarrow> x' \<in> X \<Longrightarrow> dist x x' < d \<Longrightarrow> dist (f x) (f x') < e'"
- by auto
- have "\<forall>\<^sub>F n in sequentially. dist (xs n) (xs' n) < d"
- by (auto intro!: \<open>0 < d\<close> order_tendstoD tendsto_eq_intros xs xs')
- ultimately
- show "\<forall>\<^sub>F n in sequentially. dist (f (xs' n)) l < e"
- proof eventually_elim
- case (elim n)
- have "dist (f (xs' n)) l \<le> dist (f (xs n)) (f (xs' n)) + dist (f (xs n)) l"
- by (metis dist_triangle dist_commute)
- also have "dist (f (xs n)) (f (xs' n)) < e'"
- by (auto intro!: d xs \<open>xs' _ \<in> _\<close> elim)
- also note \<open>dist (f (xs n)) l < e'\<close>
- also have "e' + e' = e" by (simp add: e'_def)
- finally show ?case by simp
- qed
- qed
- qed
- thus ?thesis ..
-qed
-
-lemma uniformly_continuous_on_extension_on_closure:
- fixes f::"'a::metric_space \<Rightarrow> 'b::complete_space"
- assumes uc: "uniformly_continuous_on X f"
- obtains g where "uniformly_continuous_on (closure X) g" "\<And>x. x \<in> X \<Longrightarrow> f x = g x"
- "\<And>Y h x. X \<subseteq> Y \<Longrightarrow> Y \<subseteq> closure X \<Longrightarrow> continuous_on Y h \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> f x = h x) \<Longrightarrow> x \<in> Y \<Longrightarrow> h x = g x"
-proof -
- from uc have cont_f: "continuous_on X f"
- by (simp add: uniformly_continuous_imp_continuous)
- obtain y where y: "(f \<longlongrightarrow> y x) (at x within X)" if "x \<in> closure X" for x
- apply atomize_elim
- apply (rule choice)
- using uniformly_continuous_on_extension_at_closure[OF assms]
- by metis
- let ?g = "\<lambda>x. if x \<in> X then f x else y x"
-
- have "uniformly_continuous_on (closure X) ?g"
- unfolding uniformly_continuous_on_def
- proof safe
- fix e::real assume "e > 0"
- define e' where "e' \<equiv> e / 3"
- have "e' > 0" using \<open>e > 0\<close> by (simp add: e'_def)
- from uc[unfolded uniformly_continuous_on_def, rule_format, OF \<open>0 < e'\<close>]
- obtain d where "d > 0" and d: "\<And>x x'. x \<in> X \<Longrightarrow> x' \<in> X \<Longrightarrow> dist x' x < d \<Longrightarrow> dist (f x') (f x) < e'"
- by auto
- define d' where "d' = d / 3"
- have "d' > 0" using \<open>d > 0\<close> by (simp add: d'_def)
- show "\<exists>d>0. \<forall>x\<in>closure X. \<forall>x'\<in>closure X. dist x' x < d \<longrightarrow> dist (?g x') (?g x) < e"
- proof (safe intro!: exI[where x=d'] \<open>d' > 0\<close>)
- fix x x' assume x: "x \<in> closure X" and x': "x' \<in> closure X" and dist: "dist x' x < d'"
- then obtain xs xs' where xs: "xs \<longlonglongrightarrow> x" "\<And>n. xs n \<in> X"
- and xs': "xs' \<longlonglongrightarrow> x'" "\<And>n. xs' n \<in> X"
- by (auto simp: closure_sequential)
- have "\<forall>\<^sub>F n in sequentially. dist (xs' n) x' < d'"
- and "\<forall>\<^sub>F n in sequentially. dist (xs n) x < d'"
- by (auto intro!: \<open>0 < d'\<close> order_tendstoD tendsto_eq_intros xs xs')
- moreover
- have "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> y x" if "x \<in> closure X" "x \<notin> X" "xs \<longlonglongrightarrow> x" "\<And>n. xs n \<in> X" for xs x
- using that not_eventuallyD
- by (force intro!: filterlim_compose[OF y[OF \<open>x \<in> closure X\<close>]] simp: filterlim_at)
- then have "(\<lambda>x. f (xs' x)) \<longlonglongrightarrow> ?g x'" "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> ?g x"
- using x x'
- by (auto intro!: continuous_on_tendsto_compose[OF cont_f] simp: xs' xs)
- then have "\<forall>\<^sub>F n in sequentially. dist (f (xs' n)) (?g x') < e'"
- "\<forall>\<^sub>F n in sequentially. dist (f (xs n)) (?g x) < e'"
- by (auto intro!: \<open>0 < e'\<close> order_tendstoD tendsto_eq_intros)
- ultimately
- have "\<forall>\<^sub>F n in sequentially. dist (?g x') (?g x) < e"
- proof eventually_elim
- case (elim n)
- have "dist (?g x') (?g x) \<le>
- dist (f (xs' n)) (?g x') + dist (f (xs' n)) (f (xs n)) + dist (f (xs n)) (?g x)"
- by (metis add.commute add_le_cancel_left dist_commute dist_triangle dist_triangle_le)
- also
- {
- have "dist (xs' n) (xs n) \<le> dist (xs' n) x' + dist x' x + dist (xs n) x"
- by (metis add.commute add_le_cancel_left dist_triangle dist_triangle_le)
- also note \<open>dist (xs' n) x' < d'\<close>
- also note \<open>dist x' x < d'\<close>
- also note \<open>dist (xs n) x < d'\<close>
- finally have "dist (xs' n) (xs n) < d" by (simp add: d'_def)
- }
- with \<open>xs _ \<in> X\<close> \<open>xs' _ \<in> X\<close> have "dist (f (xs' n)) (f (xs n)) < e'"
- by (rule d)
- also note \<open>dist (f (xs' n)) (?g x') < e'\<close>
- also note \<open>dist (f (xs n)) (?g x) < e'\<close>
- finally show ?case by (simp add: e'_def)
- qed
- then show "dist (?g x') (?g x) < e" by simp
- qed
- qed
- moreover have "f x = ?g x" if "x \<in> X" for x using that by simp
- moreover
- {
- fix Y h x
- assume Y: "x \<in> Y" "X \<subseteq> Y" "Y \<subseteq> closure X" and cont_h: "continuous_on Y h"
- and extension: "(\<And>x. x \<in> X \<Longrightarrow> f x = h x)"
- {
- assume "x \<notin> X"
- have "x \<in> closure X" using Y by auto
- then obtain xs where xs: "xs \<longlonglongrightarrow> x" "\<And>n. xs n \<in> X"
- by (auto simp: closure_sequential)
- from continuous_on_tendsto_compose[OF cont_h xs(1)] xs(2) Y
- have hx: "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> h x"
- by (auto simp: set_mp extension)
- then have "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> y x"
- using \<open>x \<notin> X\<close> not_eventuallyD xs(2)
- by (force intro!: filterlim_compose[OF y[OF \<open>x \<in> closure X\<close>]] simp: filterlim_at xs)
- with hx have "h x = y x" by (rule LIMSEQ_unique)
- } then
- have "h x = ?g x"
- using extension by auto
- }
- ultimately show ?thesis ..
-qed
-
-lemma bounded_uniformly_continuous_image:
- fixes f :: "'a :: heine_borel \<Rightarrow> 'b :: heine_borel"
- assumes "uniformly_continuous_on S f" "bounded S"
- shows "bounded(f ` S)"
- by (metis (no_types, lifting) assms bounded_closure_image compact_closure compact_continuous_image compact_eq_bounded_closed image_cong uniformly_continuous_imp_continuous uniformly_continuous_on_extension_on_closure)
-
-subsection%unimportant \<open>Making a continuous function avoid some value in a neighbourhood\<close>
-
-lemma continuous_within_avoid:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::t1_space"
- assumes "continuous (at x within s) f"
- and "f x \<noteq> a"
- shows "\<exists>e>0. \<forall>y \<in> s. dist x y < e --> f y \<noteq> a"
-proof -
- obtain U where "open U" and "f x \<in> U" and "a \<notin> U"
- using t1_space [OF \<open>f x \<noteq> a\<close>] by fast
- have "(f \<longlongrightarrow> f x) (at x within s)"
- using assms(1) by (simp add: continuous_within)
- then have "eventually (\<lambda>y. f y \<in> U) (at x within s)"
- using \<open>open U\<close> and \<open>f x \<in> U\<close>
- unfolding tendsto_def by fast
- then have "eventually (\<lambda>y. f y \<noteq> a) (at x within s)"
- using \<open>a \<notin> U\<close> by (fast elim: eventually_mono)
- then show ?thesis
- using \<open>f x \<noteq> a\<close> by (auto simp: dist_commute eventually_at)
-qed
-
-lemma continuous_at_avoid:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::t1_space"
- assumes "continuous (at x) f"
- and "f x \<noteq> a"
- shows "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> f y \<noteq> a"
- using assms continuous_within_avoid[of x UNIV f a] by simp
-
-lemma continuous_on_avoid:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::t1_space"
- assumes "continuous_on s f"
- and "x \<in> s"
- and "f x \<noteq> a"
- shows "\<exists>e>0. \<forall>y \<in> s. dist x y < e \<longrightarrow> f y \<noteq> a"
- using assms(1)[unfolded continuous_on_eq_continuous_within, THEN bspec[where x=x],
- OF assms(2)] continuous_within_avoid[of x s f a]
- using assms(3)
- by auto
-
-lemma continuous_on_open_avoid:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::t1_space"
- assumes "continuous_on s f"
- and "open s"
- and "x \<in> s"
- and "f x \<noteq> a"
- shows "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> f y \<noteq> a"
- using assms(1)[unfolded continuous_on_eq_continuous_at[OF assms(2)], THEN bspec[where x=x], OF assms(3)]
- using continuous_at_avoid[of x f a] assms(4)
- by auto
-
subsection%unimportant\<open>Quotient maps\<close>
lemma quotient_map_imp_continuous_open: