--- 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:
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy Sun Jan 06 16:27:52 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy Sun Jan 06 17:54:49 2019 +0100
@@ -43,6 +43,7 @@
from power2_le_imp_le[OF th yz] show ?thesis .
qed
+
subsection \<open>Combination of Elementary and Abstract Topology\<close>
lemma closedin_limpt:
@@ -132,8 +133,51 @@
\<Longrightarrow> openin (subtopology euclidean u) (s - {a})"
by (metis Int_Diff open_delete openin_open)
+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 \<open>Continuity\<close>
+
+subsubsection \<open>Continuity\<close>
lemma interior_image_subset:
assumes "inj f" "\<And>x. continuous (at x) f"
@@ -153,6 +197,66 @@
with \<open>x = f y\<close> show "x \<in> f ` interior S" ..
qed
+subsubsection%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
+
+subsubsection%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 \<open>Open and closed balls\<close>
definition%important ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
@@ -182,24 +286,12 @@
lemma sphere_trivial [simp]: "sphere x 0 = {x}"
by (simp add: sphere_def)
-lemma mem_ball_0 [simp]: "x \<in> ball 0 e \<longleftrightarrow> norm x < e"
- for x :: "'a::real_normed_vector"
- by (simp add: dist_norm)
-
-lemma mem_cball_0 [simp]: "x \<in> cball 0 e \<longleftrightarrow> norm x \<le> e"
- for x :: "'a::real_normed_vector"
- by (simp add: dist_norm)
-
lemma disjoint_ballI: "dist x y \<ge> r+s \<Longrightarrow> ball x r \<inter> ball y s = {}"
using dist_triangle_less_add not_le by fastforce
lemma disjoint_cballI: "dist x y > r + s \<Longrightarrow> cball x r \<inter> cball y s = {}"
by (metis add_mono disjoint_iff_not_equal dist_triangle2 dual_order.trans leD mem_cball)
-lemma mem_sphere_0 [simp]: "x \<in> sphere 0 e \<longleftrightarrow> norm x = e"
- for x :: "'a::real_normed_vector"
- by (simp add: dist_norm)
-
lemma sphere_empty [simp]: "r < 0 \<Longrightarrow> sphere a r = {}"
for a :: "'a::metric_space"
by auto
@@ -259,24 +351,6 @@
lemma cball_diff_eq_sphere: "cball a r - ball a r = sphere a r"
by (auto simp: cball_def ball_def dist_commute)
-lemma image_add_ball [simp]:
- fixes a :: "'a::real_normed_vector"
- shows "(+) b ` ball a r = ball (a+b) r"
-apply (intro equalityI subsetI)
-apply (force simp: dist_norm)
-apply (rule_tac x="x-b" in image_eqI)
-apply (auto simp: dist_norm algebra_simps)
-done
-
-lemma image_add_cball [simp]:
- fixes a :: "'a::real_normed_vector"
- shows "(+) b ` cball a r = cball (a+b) r"
-apply (intro equalityI subsetI)
-apply (force simp: dist_norm)
-apply (rule_tac x="x-b" in image_eqI)
-apply (auto simp: dist_norm algebra_simps)
-done
-
lemma open_ball [intro, simp]: "open (ball x e)"
proof -
have "open (dist x -` {..<e})"
@@ -362,6 +436,42 @@
shows "{a <..< b} = ball ((a + b)/2) ((b - a)/2)"
by (auto simp: dist_real_def field_simps mem_ball)
+lemma interior_ball [simp]: "interior (ball x e) = ball x e"
+ by (simp add: interior_open)
+
+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_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
+
subsection \<open>Limit Points\<close>
@@ -377,10 +487,6 @@
THEN arg_cong [where f=Not]]
by (simp add: Bex_def conj_commute conj_left_commute)
-lemma perfect_choose_dist: "0 < r \<Longrightarrow> \<exists>a. a \<noteq> x \<and> dist a x < r"
- for x :: "'a::{perfect_space,metric_space}"
- using islimpt_UNIV [of x] by (simp add: islimpt_approachable)
-
lemma limpt_of_limpts: "x islimpt {y. y islimpt S} \<Longrightarrow> x islimpt S"
for x :: "'a::metric_space"
apply (clarsimp simp add: islimpt_approachable)
@@ -410,6 +516,25 @@
by (metis open_ball centre_in_ball finite_Int inf.absorb_iff2 inf_assoc open_contains_cball_eq)
+subsection \<open>Perfect Metric Spaces\<close>
+
+lemma perfect_choose_dist: "0 < r \<Longrightarrow> \<exists>a. a \<noteq> x \<and> dist a x < r"
+ for x :: "'a::{perfect_space,metric_space}"
+ using islimpt_UNIV [of x] by (simp add: islimpt_approachable)
+
+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
+
+
subsection \<open>?\<close>
lemma finite_ball_include:
@@ -484,6 +609,10 @@
using open_contains_ball_eq [where S="interior S"]
by (simp add: open_subset_interior)
+lemma mem_interior_cball: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. cball x e \<subseteq> S)"
+ by (meson ball_subset_cball interior_subset mem_interior open_contains_cball open_interior
+ subset_trans)
+
subsection \<open>Frontier\<close>
@@ -835,6 +964,50 @@
by (rule closed_subset_contains_Inf)
(auto intro: closed_real_atLeastAtMost intro!: bdd_belowI[of A a])
+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_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 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)
+
+
subsection \<open>Compactness\<close>
lemma compact_imp_bounded:
@@ -1134,6 +1307,7 @@
using l r by fast
qed
+
subsubsection \<open>Completeness\<close>
proposition (in metric_space) completeI:
@@ -1392,6 +1566,297 @@
using frontier_subset_closed compact_eq_bounded_closed
by blast
+
+subsubsection \<open>Properties of Balls and Spheres\<close>
+
+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
+
+
+subsubsection \<open>Distance 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 \<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 \<open>Continuity\<close>
text\<open>Derive the epsilon-delta forms, which we often use as "definitions"\<close>
@@ -1633,6 +2098,267 @@
unfolding dist_norm tendsto_norm_zero_iff diff[symmetric]
by (auto intro: tendsto_zero)
+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 \<open>With Abstract Topology (TODO: move and remove dependency?)\<close>
@@ -1837,4 +2563,171 @@
shows "continuous (at a within T) g"
using assms by (simp add: Lim_transform_within_openin continuous_within)
+
+subsection \<open>Closed Nest\<close>
+
+text \<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%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
+
+
end
\ No newline at end of file
--- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy Sun Jan 06 16:27:52 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy Sun Jan 06 17:54:49 2019 +0100
@@ -136,6 +136,296 @@
qed
qed
+subsection \<open>Limit Points\<close>
+
+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
+ 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
+ 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
+
+
+subsection \<open>Balls and Spheres in Normed Spaces\<close>
+
+lemma mem_ball_0 [simp]: "x \<in> ball 0 e \<longleftrightarrow> norm x < e"
+ for x :: "'a::real_normed_vector"
+ by (simp add: dist_norm)
+
+lemma mem_cball_0 [simp]: "x \<in> cball 0 e \<longleftrightarrow> norm x \<le> e"
+ for x :: "'a::real_normed_vector"
+ by (simp add: dist_norm)
+
+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
+
+lemma mem_sphere_0 [simp]: "x \<in> sphere 0 e \<longleftrightarrow> norm x = e"
+ for x :: "'a::real_normed_vector"
+ by (simp add: dist_norm)
+
+(* 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
+ have "cball x e = {}"
+ proof (rule equals0I)
+ fix y
+ assume "y \<in> cball x e"
+ then show False
+ by (metis ball_eq_empty null cs dist_eq_0_iff dist_le_zero_iff empty_subsetI mem_cball
+ subset_antisym subset_ball)
+ qed
+ 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 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)
+
+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)
+
+lemma image_add_ball [simp]:
+ fixes a :: "'a::real_normed_vector"
+ shows "(+) b ` ball a r = ball (a+b) r"
+apply (intro equalityI subsetI)
+apply (force simp: dist_norm)
+apply (rule_tac x="x-b" in image_eqI)
+apply (auto simp: dist_norm algebra_simps)
+done
+
+lemma image_add_cball [simp]:
+ fixes a :: "'a::real_normed_vector"
+ shows "(+) b ` cball a r = cball (a+b) r"
+apply (intro equalityI subsetI)
+apply (force simp: dist_norm)
+apply (rule_tac x="x-b" in image_eqI)
+apply (auto simp: dist_norm algebra_simps)
+done
+
subsection%unimportant \<open>Various Lemmas on Normed Algebras\<close>
@@ -181,6 +471,14 @@
apply (drule_tac x=UNIV in spec, simp)
done
+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)
+
+
subsection \<open>Limits\<close>
proposition Lim_at_infinity: "(f \<longlongrightarrow> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x \<ge> b \<longrightarrow> dist (f x) l < e)"
@@ -326,6 +624,19 @@
subsection \<open>Boundedness\<close>
+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 bounded_pos: "bounded S \<longleftrightarrow> (\<exists>b>0. \<forall>x\<in> S. norm x \<le> b)"
apply (simp add: bounded_iff)
apply (subgoal_tac "\<And>x (y::real). 0 < 1 + \<bar>y\<bar> \<and> (x \<le> y \<longrightarrow> x \<le> 1 + \<bar>y\<bar>)")
@@ -463,6 +774,33 @@
shows "bounded (- S) \<Longrightarrow> \<not> bounded S"
using bounded_Un [of S "-S"] by (simp add: sup_compl_top)
+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 \<open>Normed spaces with the Heine-Borel property\<close>
@@ -492,6 +830,193 @@
by (metis of_nat_le_iff Int_subset_iff \<open>K \<subseteq> S\<close> real_arch_simple subset_cball subset_trans)
qed auto
+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 \<open>Continuity\<close>
--- a/src/HOL/Analysis/Elementary_Topology.thy Sun Jan 06 16:27:52 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Topology.thy Sun Jan 06 17:54:49 2019 +0100
@@ -2096,4 +2096,5 @@
using T_def by (auto elim!: eventually_mono)
qed
+
end
\ No newline at end of file
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Sun Jan 06 16:27:52 2019 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Sun Jan 06 17:54:49 2019 +0100
@@ -715,58 +715,21 @@
using is_interval_translation[of "-c" X]
by (metis image_cong uminus_add_conv_diff)
-lemma compact_lemma:
- fixes f :: "nat \<Rightarrow> 'a::euclidean_space"
- assumes "bounded (range f)"
- shows "\<forall>d\<subseteq>Basis. \<exists>l::'a. \<exists> r.
- strict_mono r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)"
- by (rule compact_lemma_general[where unproj="\<lambda>e. \<Sum>i\<in>Basis. e i *\<^sub>R i"])
- (auto intro!: assms bounded_linear_inner_left bounded_linear_image
- simp: euclidean_representation)
+
+subsection%unimportant \<open>Bounded Projections\<close>
-instance%important euclidean_space \<subseteq> heine_borel
-proof%unimportant
- fix f :: "nat \<Rightarrow> 'a"
- assume f: "bounded (range f)"
- then obtain l::'a and r where r: "strict_mono r"
- and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially"
- using compact_lemma [OF f] by blast
- {
- fix e::real
- assume "e > 0"
- hence "e / real_of_nat DIM('a) > 0" by (simp add: DIM_positive)
- with l have "eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e / (real_of_nat DIM('a))) sequentially"
- by simp
- moreover
- {
- fix n
- assume n: "\<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e / (real_of_nat DIM('a))"
- have "dist (f (r n)) l \<le> (\<Sum>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i))"
- apply (subst euclidean_dist_l2)
- using zero_le_dist
- apply (rule L2_set_le_sum)
- done
- also have "\<dots> < (\<Sum>i\<in>(Basis::'a set). e / (real_of_nat DIM('a)))"
- apply (rule sum_strict_mono)
- using n
- apply auto
- done
- finally have "dist (f (r n)) l < e"
- by auto
- }
- ultimately have "eventually (\<lambda>n. dist (f (r n)) l < e) sequentially"
- by (rule eventually_mono)
- }
- then have *: "((f \<circ> r) \<longlongrightarrow> l) sequentially"
- unfolding o_def tendsto_iff by simp
- with r show "\<exists>l r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
- by auto
-qed
+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)
-instance euclidean_space \<subseteq> banach ..
+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)
-subsubsection%unimportant \<open>Structural rules for pointwise continuity\<close>
+subsection%unimportant \<open>Structural rules for pointwise continuity\<close>
lemma continuous_infnorm[continuous_intros]:
"continuous F f \<Longrightarrow> continuous F (\<lambda>x. infnorm (f x))"
@@ -779,7 +742,7 @@
using assms unfolding continuous_def by (rule tendsto_inner)
-subsubsection%unimportant \<open>Structural rules for setwise continuity\<close>
+subsection%unimportant \<open>Structural rules for setwise continuity\<close>
lemma continuous_on_infnorm[continuous_intros]:
"continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. infnorm (f x))"
@@ -793,9 +756,7 @@
using bounded_bilinear_inner assms
by (rule bounded_bilinear.continuous_on)
-subsection%unimportant \<open>Intervals\<close>
-
-text \<open>Openness of halfspaces.\<close>
+subsection \<open>Openness of halfspaces.\<close>
lemma open_halfspace_lt: "open {x. inner a x < b}"
by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id)
@@ -809,7 +770,19 @@
lemma open_halfspace_component_gt: "open {x::'a::euclidean_space. x\<bullet>i > a}"
by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id)
-text \<open>This gives a simple derivation of limit component bounds.\<close>
+lemma eucl_less_eq_halfspaces:
+ fixes a :: "'a::euclidean_space"
+ shows "{x. x <e a} = (\<Inter>i\<in>Basis. {x. x \<bullet> i < a \<bullet> i})"
+ "{x. a <e x} = (\<Inter>i\<in>Basis. {x. a \<bullet> i < x \<bullet> i})"
+ by (auto simp: eucl_less_def)
+
+lemma open_Collect_eucl_less[simp, intro]:
+ fixes a :: "'a::euclidean_space"
+ shows "open {x. x <e a}" "open {x. a <e x}"
+ by (auto simp: eucl_less_eq_halfspaces open_halfspace_component_lt open_halfspace_component_gt)
+
+
+subsection \<open>Limit Component Bounds\<close>
lemma open_box[intro]: "open (box a b)"
proof -
@@ -820,40 +793,6 @@
finally show ?thesis .
qed
-instance euclidean_space \<subseteq> second_countable_topology
-proof
- define a where "a f = (\<Sum>i\<in>Basis. fst (f i) *\<^sub>R i)" for f :: "'a \<Rightarrow> real \<times> real"
- then have a: "\<And>f. (\<Sum>i\<in>Basis. fst (f i) *\<^sub>R i) = a f"
- by simp
- define b where "b f = (\<Sum>i\<in>Basis. snd (f i) *\<^sub>R i)" for f :: "'a \<Rightarrow> real \<times> real"
- then have b: "\<And>f. (\<Sum>i\<in>Basis. snd (f i) *\<^sub>R i) = b f"
- by simp
- define B where "B = (\<lambda>f. box (a f) (b f)) ` (Basis \<rightarrow>\<^sub>E (\<rat> \<times> \<rat>))"
-
- have "Ball B open" by (simp add: B_def open_box)
- moreover have "(\<forall>A. open A \<longrightarrow> (\<exists>B'\<subseteq>B. \<Union>B' = A))"
- proof safe
- fix A::"'a set"
- assume "open A"
- show "\<exists>B'\<subseteq>B. \<Union>B' = A"
- apply (rule exI[of _ "{b\<in>B. b \<subseteq> A}"])
- apply (subst (3) open_UNION_box[OF \<open>open A\<close>])
- apply (auto simp: a b B_def)
- done
- qed
- ultimately
- have "topological_basis B"
- unfolding topological_basis_def by blast
- moreover
- have "countable B"
- unfolding B_def
- by (intro countable_image countable_PiE finite_Basis countable_SIGMA countable_rat)
- ultimately show "\<exists>B::'a set set. countable B \<and> open = generate_topology B"
- by (blast intro: topological_basis_imp_subbasis)
-qed
-
-instance euclidean_space \<subseteq> polish_space ..
-
lemma closed_cbox[intro]:
fixes a b :: "'a::euclidean_space"
shows "closed (cbox a b)"
@@ -939,12 +878,6 @@
shows "UNIV \<noteq> cbox a b" "UNIV \<noteq> box a b"
using bounded_box[of a b] bounded_cbox[of a b] by force+
-lemma compact_cbox [simp]:
- fixes a :: "'a::euclidean_space"
- shows "compact (cbox a b)"
- using bounded_closed_imp_seq_compact[of "cbox a b"] using bounded_cbox[of a b]
- by (auto simp: compact_eq_seq_compact_metric)
-
lemma box_midpoint:
fixes a :: "'a::euclidean_space"
assumes "box a b \<noteq> {}"
@@ -1107,16 +1040,259 @@
unfolding closure_box[OF assms, symmetric]
unfolding open_Int_closure_eq_empty[OF open_box] ..
-lemma eucl_less_eq_halfspaces:
+subsection \<open>Class Instances\<close>
+
+lemma compact_lemma:
+ fixes f :: "nat \<Rightarrow> 'a::euclidean_space"
+ assumes "bounded (range f)"
+ shows "\<forall>d\<subseteq>Basis. \<exists>l::'a. \<exists> r.
+ strict_mono r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)"
+ by (rule compact_lemma_general[where unproj="\<lambda>e. \<Sum>i\<in>Basis. e i *\<^sub>R i"])
+ (auto intro!: assms bounded_linear_inner_left bounded_linear_image
+ simp: euclidean_representation)
+
+instance%important euclidean_space \<subseteq> heine_borel
+proof%unimportant
+ fix f :: "nat \<Rightarrow> 'a"
+ assume f: "bounded (range f)"
+ then obtain l::'a and r where r: "strict_mono r"
+ and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially"
+ using compact_lemma [OF f] by blast
+ {
+ fix e::real
+ assume "e > 0"
+ hence "e / real_of_nat DIM('a) > 0" by (simp add: DIM_positive)
+ with l have "eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e / (real_of_nat DIM('a))) sequentially"
+ by simp
+ moreover
+ {
+ fix n
+ assume n: "\<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e / (real_of_nat DIM('a))"
+ have "dist (f (r n)) l \<le> (\<Sum>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i))"
+ apply (subst euclidean_dist_l2)
+ using zero_le_dist
+ apply (rule L2_set_le_sum)
+ done
+ also have "\<dots> < (\<Sum>i\<in>(Basis::'a set). e / (real_of_nat DIM('a)))"
+ apply (rule sum_strict_mono)
+ using n
+ apply auto
+ done
+ finally have "dist (f (r n)) l < e"
+ by auto
+ }
+ ultimately have "eventually (\<lambda>n. dist (f (r n)) l < e) sequentially"
+ by (rule eventually_mono)
+ }
+ then have *: "((f \<circ> r) \<longlongrightarrow> l) sequentially"
+ unfolding o_def tendsto_iff by simp
+ with r show "\<exists>l r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
+ by auto
+qed
+
+instance%important euclidean_space \<subseteq> banach ..
+
+instance euclidean_space \<subseteq> second_countable_topology
+proof
+ define a where "a f = (\<Sum>i\<in>Basis. fst (f i) *\<^sub>R i)" for f :: "'a \<Rightarrow> real \<times> real"
+ then have a: "\<And>f. (\<Sum>i\<in>Basis. fst (f i) *\<^sub>R i) = a f"
+ by simp
+ define b where "b f = (\<Sum>i\<in>Basis. snd (f i) *\<^sub>R i)" for f :: "'a \<Rightarrow> real \<times> real"
+ then have b: "\<And>f. (\<Sum>i\<in>Basis. snd (f i) *\<^sub>R i) = b f"
+ by simp
+ define B where "B = (\<lambda>f. box (a f) (b f)) ` (Basis \<rightarrow>\<^sub>E (\<rat> \<times> \<rat>))"
+
+ have "Ball B open" by (simp add: B_def open_box)
+ moreover have "(\<forall>A. open A \<longrightarrow> (\<exists>B'\<subseteq>B. \<Union>B' = A))"
+ proof safe
+ fix A::"'a set"
+ assume "open A"
+ show "\<exists>B'\<subseteq>B. \<Union>B' = A"
+ apply (rule exI[of _ "{b\<in>B. b \<subseteq> A}"])
+ apply (subst (3) open_UNION_box[OF \<open>open A\<close>])
+ apply (auto simp: a b B_def)
+ done
+ qed
+ ultimately
+ have "topological_basis B"
+ unfolding topological_basis_def by blast
+ moreover
+ have "countable B"
+ unfolding B_def
+ by (intro countable_image countable_PiE finite_Basis countable_SIGMA countable_rat)
+ ultimately show "\<exists>B::'a set set. countable B \<and> open = generate_topology B"
+ by (blast intro: topological_basis_imp_subbasis)
+qed
+
+instance euclidean_space \<subseteq> polish_space ..
+
+
+subsection \<open>Compact Boxes\<close>
+
+lemma compact_cbox [simp]:
fixes a :: "'a::euclidean_space"
- shows "{x. x <e a} = (\<Inter>i\<in>Basis. {x. x \<bullet> i < a \<bullet> i})"
- "{x. a <e x} = (\<Inter>i\<in>Basis. {x. a \<bullet> i < x \<bullet> i})"
- by (auto simp: eucl_less_def)
+ shows "compact (cbox a b)"
+ using bounded_closed_imp_seq_compact[of "cbox a b"] using bounded_cbox[of a b]
+ by (auto simp: compact_eq_seq_compact_metric)
+
+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
+
+
+subsection%unimportant\<open>Relating linear images to open/closed/interior/closure\<close>
-lemma open_Collect_eucl_less[simp, intro]:
- fixes a :: "'a::euclidean_space"
- shows "open {x. x <e a}" "open {x. a <e x}"
- by (auto simp: eucl_less_eq_halfspaces open_halfspace_component_lt open_halfspace_component_gt)
+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)
no_notation
eucl_less (infix "<e" 50)
--- a/src/HOL/Conditionally_Complete_Lattices.thy Sun Jan 06 16:27:52 2019 +0100
+++ b/src/HOL/Conditionally_Complete_Lattices.thy Sun Jan 06 17:54:49 2019 +0100
@@ -481,6 +481,36 @@
lemma cInf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x::'a::{conditionally_complete_linorder, dense_linorder}} = y"
by (auto intro!: cInf_eq_non_empty intro: dense_ge_bounded)
+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 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 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)
+
class linear_continuum = conditionally_complete_linorder + dense_linorder +
assumes UNIV_not_singleton: "\<exists>a b::'a. a \<noteq> b"
begin