diff --git a/src/HOL/Analysis/Abstract_Topology_2.thy b/src/HOL/Analysis/Abstract_Topology_2.thy --- a/src/HOL/Analysis/Abstract_Topology_2.thy +++ b/src/HOL/Analysis/Abstract_Topology_2.thy @@ -1,1616 +1,1601 @@ (* Author: L C Paulson, University of Cambridge Author: Amine Chaieb, University of Cambridge Author: Robert Himmelmann, TU Muenchen Author: Brian Huffman, Portland State University *) section \Abstract Topology 2\ theory Abstract_Topology_2 imports Elementary_Topology Abstract_Topology "HOL-Library.Indicator_Function" begin text \Combination of Elementary and Abstract Topology\ -(* FIXME: move elsewhere *) - -lemma approachable_lt_le: "(\(d::real) > 0. \x. f x < d \ P x) \ (\d>0. \x. f x \ d \ P x)" - apply auto - apply (rule_tac x="d/2" in exI) - apply auto - done - -lemma approachable_lt_le2: \ \like the above, but pushes aside an extra formula\ +lemma approachable_lt_le2: "(\(d::real) > 0. \x. Q x \ f x < d \ P x) \ (\d>0. \x. f x \ d \ Q x \ P x)" apply auto apply (rule_tac x="d/2" in exI, auto) done lemma triangle_lemma: fixes x y z :: real assumes x: "0 \ x" and y: "0 \ y" and z: "0 \ z" and xy: "x\<^sup>2 \ y\<^sup>2 + z\<^sup>2" shows "x \ y + z" proof - have "y\<^sup>2 + z\<^sup>2 \ y\<^sup>2 + 2 * y * z + z\<^sup>2" using z y by simp with xy have th: "x\<^sup>2 \ (y + z)\<^sup>2" by (simp add: power2_eq_square field_simps) from y z have yz: "y + z \ 0" by arith from power2_le_imp_le[OF th yz] show ?thesis . qed lemma isCont_indicator: fixes x :: "'a::t2_space" shows "isCont (indicator A :: 'a \ real) x = (x \ frontier A)" proof auto fix x assume cts_at: "isCont (indicator A :: 'a \ real) x" and fr: "x \ frontier A" with continuous_at_open have 1: "\V::real set. open V \ indicator A x \ V \ (\U::'a set. open U \ x \ U \ (\y\U. indicator A y \ V))" by auto show False proof (cases "x \ A") assume x: "x \ A" hence "indicator A x \ ({0<..<2} :: real set)" by simp hence "\U. open U \ x \ U \ (\y\U. indicator A y \ ({0<..<2} :: real set))" using 1 open_greaterThanLessThan by blast then guess U .. note U = this hence "\y\U. indicator A y > (0::real)" unfolding greaterThanLessThan_def by auto hence "U \ A" using indicator_eq_0_iff by force hence "x \ interior A" using U interiorI by auto thus ?thesis using fr unfolding frontier_def by simp next assume x: "x \ A" hence "indicator A x \ ({-1<..<1} :: real set)" by simp hence "\U. open U \ x \ U \ (\y\U. indicator A y \ ({-1<..<1} :: real set))" using 1 open_greaterThanLessThan by blast then guess U .. note U = this hence "\y\U. indicator A y < (1::real)" unfolding greaterThanLessThan_def by auto hence "U \ -A" by auto hence "x \ interior (-A)" using U interiorI by auto thus ?thesis using fr interior_complement unfolding frontier_def by auto qed next assume nfr: "x \ frontier A" hence "x \ interior A \ x \ interior (-A)" by (auto simp: frontier_def closure_interior) thus "isCont ((indicator A)::'a \ real) x" proof assume int: "x \ interior A" then obtain U where U: "open U" "x \ U" "U \ A" unfolding interior_def by auto hence "\y\U. indicator A y = (1::real)" unfolding indicator_def by auto hence "continuous_on U (indicator A)" by (simp add: indicator_eq_1_iff) thus ?thesis using U continuous_on_eq_continuous_at by auto next assume ext: "x \ interior (-A)" then obtain U where U: "open U" "x \ U" "U \ -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 closedin_limpt: "closedin (top_of_set T) S \ S \ T \ (\x. x islimpt S \ x \ T \ x \ S)" apply (simp add: closedin_closed, safe) apply (simp add: closed_limpt islimpt_subset) apply (rule_tac x="closure S" in exI, simp) apply (force simp: closure_def) done lemma closedin_closed_eq: "closed S \ closedin (top_of_set S) T \ closed T \ T \ S" by (meson closedin_limpt closed_subset closedin_closed_trans) lemma connected_closed_set: "closed S \ connected S \ (\A B. closed A \ closed B \ A \ {} \ B \ {} \ A \ B = S \ A \ B = {})" unfolding connected_closedin_eq closedin_closed_eq connected_closedin_eq by blast text \If a connnected set is written as the union of two nonempty closed sets, then these sets have to intersect.\ lemma connected_as_closed_union: assumes "connected C" "C = A \ B" "closed A" "closed B" "A \ {}" "B \ {}" shows "A \ B \ {}" by (metis assms closed_Un connected_closed_set) lemma closedin_subset_trans: "closedin (top_of_set U) S \ S \ T \ T \ U \ closedin (top_of_set T) S" by (meson closedin_limpt subset_iff) lemma openin_subset_trans: "openin (top_of_set U) S \ S \ T \ T \ U \ openin (top_of_set T) S" by (auto simp: openin_open) lemma closedin_compact: "\compact S; closedin (top_of_set S) T\ \ compact T" by (metis closedin_closed compact_Int_closed) lemma closedin_compact_eq: fixes S :: "'a::t2_space set" shows "compact S \ (closedin (top_of_set S) T \ compact T \ T \ S)" by (metis closedin_imp_subset closedin_compact closed_subset compact_imp_closed) subsection \Closure\ lemma euclidean_closure_of [simp]: "euclidean closure_of S = closure S" by (auto simp: closure_of_def closure_def islimpt_def) lemma closure_openin_Int_closure: assumes ope: "openin (top_of_set U) S" and "T \ U" shows "closure(S \ closure T) = closure(S \ T)" proof obtain V where "open V" and S: "S = U \ V" using ope using openin_open by metis show "closure (S \ closure T) \ closure (S \ T)" proof (clarsimp simp: S) fix x assume "x \ closure (U \ V \ closure T)" then have "V \ closure T \ A \ x \ closure A" for A by (metis closure_mono subsetD inf.coboundedI2 inf_assoc) then have "x \ closure (T \ V)" by (metis \open V\ closure_closure inf_commute open_Int_closure_subset) then show "x \ closure (U \ V \ T)" by (metis \T \ U\ inf.absorb_iff2 inf_assoc inf_commute) qed next show "closure (S \ T) \ closure (S \ closure T)" by (meson Int_mono closure_mono closure_subset order_refl) qed corollary infinite_openin: fixes S :: "'a :: t1_space set" shows "\openin (top_of_set U) S; x \ S; x islimpt U\ \ infinite S" by (clarsimp simp add: openin_open islimpt_eq_acc_point inf_commute) lemma closure_Int_ballI: assumes "\U. \openin (top_of_set S) U; U \ {}\ \ T \ U \ {}" shows "S \ closure T" proof (clarsimp simp: closure_iff_nhds_not_empty) fix x and A and V assume "x \ S" "V \ A" "open V" "x \ V" "T \ A = {}" then have "openin (top_of_set S) (A \ V \ S)" by (auto simp: openin_open intro!: exI[where x="V"]) moreover have "A \ V \ S \ {}" using \x \ V\ \V \ A\ \x \ S\ by auto ultimately have "T \ (A \ V \ S) \ {}" by (rule assms) with \T \ A = {}\ show False by auto qed subsection \Frontier\ lemma euclidean_interior_of [simp]: "euclidean interior_of S = interior S" by (auto simp: interior_of_def interior_def) lemma euclidean_frontier_of [simp]: "euclidean frontier_of S = frontier S" by (auto simp: frontier_of_def frontier_def) lemma connected_Int_frontier: "\connected s; s \ t \ {}; s - t \ {}\ \ (s \ frontier t \ {})" apply (simp add: frontier_interiors connected_openin, safe) apply (drule_tac x="s \ interior t" in spec, safe) apply (drule_tac [2] x="s \ interior (-t)" in spec) apply (auto simp: disjoint_eq_subset_Compl dest: interior_subset [THEN subsetD]) done subsection \Compactness\ lemma openin_delete: fixes a :: "'a :: t1_space" shows "openin (top_of_set u) s \ openin (top_of_set u) (s - {a})" by (metis Int_Diff open_delete openin_open) lemma compact_eq_openin_cover: "compact S \ (\C. (\c\C. openin (top_of_set S) c) \ S \ \C \ (\D\C. finite D \ S \ \D))" proof safe fix C assume "compact S" and "\c\C. openin (top_of_set S) c" and "S \ \C" then have "\c\{T. open T \ S \ T \ C}. open c" and "S \ \{T. open T \ S \ T \ C}" unfolding openin_open by force+ with \compact S\ obtain D where "D \ {T. open T \ S \ T \ C}" and "finite D" and "S \ \D" by (meson compactE) then have "image (\T. S \ T) D \ C \ finite (image (\T. S \ T) D) \ S \ \(image (\T. S \ T) D)" by auto then show "\D\C. finite D \ S \ \D" .. next assume 1: "\C. (\c\C. openin (top_of_set S) c) \ S \ \C \ (\D\C. finite D \ S \ \D)" show "compact S" proof (rule compactI) fix C let ?C = "image (\T. S \ T) C" assume "\t\C. open t" and "S \ \C" then have "(\c\?C. openin (top_of_set S) c) \ S \ \?C" unfolding openin_open by auto with 1 obtain D where "D \ ?C" and "finite D" and "S \ \D" by metis let ?D = "inv_into C (\T. S \ T) ` D" have "?D \ C \ finite ?D \ S \ \?D" proof (intro conjI) from \D \ ?C\ show "?D \ C" by (fast intro: inv_into_into) from \finite D\ show "finite ?D" by (rule finite_imageI) from \S \ \D\ show "S \ \?D" - apply (rule subset_trans, clarsimp) - apply (frule subsetD [OF \D \ ?C\, THEN f_inv_into_f]) - apply (erule rev_bexI, fast) - done + apply (rule subset_trans) + by (metis Int_Union Int_lower2 \D \ (\) S ` C\ image_inv_into_cancel) qed then show "\D\C. finite D \ S \ \D" .. qed qed subsection \Continuity\ lemma interior_image_subset: assumes "inj f" "\x. continuous (at x) f" shows "interior (f ` S) \ f ` (interior S)" proof fix x assume "x \ interior (f ` S)" then obtain T where as: "open T" "x \ T" "T \ f ` S" .. then have "x \ f ` S" by auto then obtain y where y: "y \ S" "x = f y" by auto have "open (f -` T)" using assms \open T\ by (simp add: continuous_at_imp_continuous_on open_vimage) moreover have "y \ vimage f T" using \x = f y\ \x \ T\ by simp moreover have "vimage f T \ S" using \T \ image f S\ \inj f\ unfolding inj_on_def subset_eq by auto ultimately have "y \ interior S" .. with \x = f y\ show "x \ f ` interior S" .. qed subsection\<^marker>\tag unimportant\ \Equality of continuous functions on closure and related results\ lemma continuous_closedin_preimage_constant: fixes f :: "_ \ 'b::t1_space" shows "continuous_on S f \ closedin (top_of_set S) {x \ 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 :: "_ \ 'b::t1_space" shows "continuous_on S f \ closed S \ closed {x \ 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 :: "_ \ 'b::t1_space" assumes "continuous_on (closure S) f" and "\x. x \ S \ f x = a" and "x \ closure S" shows "f x = a" using continuous_closed_preimage_constant[of "closure S" f a] assms closure_minimal[of S "{x \ 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) \ T" shows "f ` (closure S) \ T" proof - have "S \ {x \ closure S. f x \ T}" using assms(3) closure_subset by auto moreover have "closed (closure S \ f -` T)" using continuous_closed_preimage[OF contf] \closed T\ by auto ultimately have "closure S = (closure S \ f -` T)" using closure_minimal[of S "(closure S \ f -` T)"] by auto then show ?thesis by auto qed subsection\<^marker>\tag unimportant\ \A function constant on a set\ definition constant_on (infixl "(constant'_on)" 50) where "f constant_on A \ \y. \x\A. f x = y" lemma constant_on_subset: "\f constant_on A; B \ A\ \ f constant_on B" unfolding constant_on_def by blast lemma injective_not_constant: fixes S :: "'a::{perfect_space} set" shows "\open S; inj_on f S; f constant_on S\ \ S = {}" unfolding constant_on_def by (metis equals0I inj_on_contraD islimpt_UNIV islimpt_def) lemma constant_on_closureI: fixes f :: "_ \ '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\<^marker>\tag unimportant\ \Continuity relative to a union.\ lemma continuous_on_Un_local: "\closedin (top_of_set (s \ t)) s; closedin (top_of_set (s \ t)) t; continuous_on s f; continuous_on t f\ \ continuous_on (s \ t) f" unfolding continuous_on closedin_limpt by (metis Lim_trivial_limit Lim_within_union Un_iff trivial_limit_within) lemma continuous_on_cases_local: "\closedin (top_of_set (s \ t)) s; closedin (top_of_set (s \ t)) t; continuous_on s f; continuous_on t g; \x. \x \ s \ \P x \ x \ t \ P x\ \ f x = g x\ \ continuous_on (s \ t) (\x. if P x then f x else g x)" by (rule continuous_on_Un_local) (auto intro: continuous_on_eq) lemma continuous_on_cases_le: fixes h :: "'a :: topological_space \ real" assumes "continuous_on {t \ s. h t \ a} f" and "continuous_on {t \ s. a \ h t} g" and h: "continuous_on s h" and "\t. \t \ s; h t = a\ \ f t = g t" shows "continuous_on s (\t. if h t \ a then f(t) else g(t))" proof - have s: "s = (s \ h -` atMost a) \ (s \ h -` atLeast a)" by force have 1: "closedin (top_of_set s) (s \ h -` atMost a)" by (rule continuous_closedin_preimage [OF h closed_atMost]) have 2: "closedin (top_of_set s) (s \ h -` atLeast a)" by (rule continuous_closedin_preimage [OF h closed_atLeast]) have eq: "s \ h -` {..a} = {t \ s. h t \ a}" "s \ h -` {a..} = {t \ s. a \ h t}" by auto show ?thesis apply (rule continuous_on_subset [of s, OF _ order_refl]) apply (subst s) apply (rule continuous_on_cases_local) using 1 2 s assms apply (auto simp: eq) done qed lemma continuous_on_cases_1: fixes s :: "real set" assumes "continuous_on {t \ s. t \ a} f" and "continuous_on {t \ s. a \ t} g" and "a \ s \ f a = g a" shows "continuous_on s (\t. if t \ a then f(t) else g(t))" using assms by (auto intro: continuous_on_cases_le [where h = id, simplified]) subsection\<^marker>\tag unimportant\\Inverse function property for open/closed maps\ lemma continuous_on_inverse_open_map: assumes contf: "continuous_on S f" and imf: "f ` S = T" and injf: "\x. x \ S \ g (f x) = x" and oo: "\U. openin (top_of_set S) U \ openin (top_of_set T) (f ` U)" shows "continuous_on T g" proof - from imf injf have gTS: "g ` T = S" by force from imf injf have fU: "U \ S \ (f ` U) = T \ g -` U" for U by force show ?thesis by (simp add: continuous_on_open [of T g] gTS) (metis openin_imp_subset fU oo) qed lemma continuous_on_inverse_closed_map: assumes contf: "continuous_on S f" and imf: "f ` S = T" and injf: "\x. x \ S \ g(f x) = x" and oo: "\U. closedin (top_of_set S) U \ closedin (top_of_set T) (f ` U)" shows "continuous_on T g" proof - from imf injf have gTS: "g ` T = S" by force from imf injf have fU: "U \ S \ (f ` U) = T \ g -` U" for U by force show ?thesis by (simp add: continuous_on_closed [of T g] gTS) (metis closedin_imp_subset fU oo) qed lemma homeomorphism_injective_open_map: assumes contf: "continuous_on S f" and imf: "f ` S = T" and injf: "inj_on f S" and oo: "\U. openin (top_of_set S) U \ openin (top_of_set T) (f ` U)" obtains g where "homeomorphism S T f g" proof have "continuous_on T (inv_into S f)" by (metis contf continuous_on_inverse_open_map imf injf inv_into_f_f oo) with imf injf contf show "homeomorphism S T f (inv_into S f)" by (auto simp: homeomorphism_def) qed lemma homeomorphism_injective_closed_map: assumes contf: "continuous_on S f" and imf: "f ` S = T" and injf: "inj_on f S" and oo: "\U. closedin (top_of_set S) U \ closedin (top_of_set T) (f ` U)" obtains g where "homeomorphism S T f g" proof have "continuous_on T (inv_into S f)" by (metis contf continuous_on_inverse_closed_map imf injf inv_into_f_f oo) with imf injf contf show "homeomorphism S T f (inv_into S f)" by (auto simp: homeomorphism_def) qed lemma homeomorphism_imp_open_map: assumes hom: "homeomorphism S T f g" and oo: "openin (top_of_set S) U" shows "openin (top_of_set T) (f ` U)" proof - from hom oo have [simp]: "f ` U = T \ g -` U" using openin_subset by (fastforce simp: homeomorphism_def rev_image_eqI) from hom have "continuous_on T g" unfolding homeomorphism_def by blast moreover have "g ` T = S" by (metis hom homeomorphism_def) ultimately show ?thesis by (simp add: continuous_on_open oo) qed lemma homeomorphism_imp_closed_map: assumes hom: "homeomorphism S T f g" and oo: "closedin (top_of_set S) U" shows "closedin (top_of_set T) (f ` U)" proof - from hom oo have [simp]: "f ` U = T \ g -` U" using closedin_subset by (fastforce simp: homeomorphism_def rev_image_eqI) from hom have "continuous_on T g" unfolding homeomorphism_def by blast moreover have "g ` T = S" by (metis hom homeomorphism_def) ultimately show ?thesis by (simp add: continuous_on_closed oo) qed subsection\<^marker>\tag unimportant\ \Seperability\ lemma subset_second_countable: obtains \ :: "'a:: second_countable_topology set set" where "countable \" "{} \ \" "\C. C \ \ \ openin(top_of_set S) C" "\T. openin(top_of_set S) T \ \\. \ \ \ \ T = \\" proof - obtain \ :: "'a set set" where "countable \" and opeB: "\C. C \ \ \ openin(top_of_set S) C" and \: "\T. openin(top_of_set S) T \ \\. \ \ \ \ T = \\" proof - obtain \ :: "'a set set" where "countable \" and ope: "\C. C \ \ \ open C" and \: "\S. open S \ \U. U \ \ \ S = \U" by (metis univ_second_countable that) show ?thesis proof show "countable ((\C. S \ C) ` \)" by (simp add: \countable \\) show "\C. C \ (\) S ` \ \ openin (top_of_set S) C" using ope by auto show "\T. openin (top_of_set S) T \ \\\(\) S ` \. T = \\" by (metis \ image_mono inf_Sup openin_open) qed qed show ?thesis proof show "countable (\ - {{}})" using \countable \\ by blast show "\C. \C \ \ - {{}}\ \ openin (top_of_set S) C" by (simp add: \\C. C \ \ \ openin (top_of_set S) C\) show "\\\\ - {{}}. T = \\" if "openin (top_of_set S) T" for T using \ [OF that] apply clarify apply (rule_tac x="\ - {{}}" in exI, auto) done qed auto qed lemma Lindelof_openin: fixes \ :: "'a::second_countable_topology set set" assumes "\S. S \ \ \ openin (top_of_set U) S" obtains \' where "\' \ \" "countable \'" "\\' = \\" proof - have "\S. S \ \ \ \T. open T \ S = U \ T" using assms by (simp add: openin_open) then obtain tf where tf: "\S. S \ \ \ open (tf S) \ (S = U \ tf S)" by metis have [simp]: "\\'. \' \ \ \ \\' = U \ \(tf ` \')" using tf by fastforce obtain \ where "countable \ \ \ \ tf ` \" "\\ = \(tf ` \)" using tf by (force intro: Lindelof [of "tf ` \"]) then obtain \' where \': "\' \ \" "countable \'" "\\' = \\" by (clarsimp simp add: countable_subset_image) then show ?thesis .. qed subsection\<^marker>\tag unimportant\\Closed Maps\ lemma continuous_imp_closed_map: fixes f :: "'a::t2_space \ 'b::t2_space" assumes "closedin (top_of_set S) U" "continuous_on S f" "f ` S = T" "compact S" shows "closedin (top_of_set T) (f ` U)" by (metis assms closedin_compact_eq compact_continuous_image continuous_on_subset subset_image_iff) lemma closed_map_restrict: assumes cloU: "closedin (top_of_set (S \ f -` T')) U" and cc: "\U. closedin (top_of_set S) U \ closedin (top_of_set T) (f ` U)" and "T' \ T" shows "closedin (top_of_set T') (f ` U)" proof - obtain V where "closed V" "U = S \ f -` T' \ V" using cloU by (auto simp: closedin_closed) with cc [of "S \ V"] \T' \ T\ show ?thesis by (fastforce simp add: closedin_closed) qed subsection\<^marker>\tag unimportant\\Open Maps\ lemma open_map_restrict: assumes opeU: "openin (top_of_set (S \ f -` T')) U" and oo: "\U. openin (top_of_set S) U \ openin (top_of_set T) (f ` U)" and "T' \ T" shows "openin (top_of_set T') (f ` U)" proof - obtain V where "open V" "U = S \ f -` T' \ V" using opeU by (auto simp: openin_open) with oo [of "S \ V"] \T' \ T\ show ?thesis by (fastforce simp add: openin_open) qed subsection\<^marker>\tag unimportant\\Quotient maps\ lemma quotient_map_imp_continuous_open: assumes T: "f ` S \ T" and ope: "\U. U \ T \ (openin (top_of_set S) (S \ f -` U) \ openin (top_of_set T) U)" shows "continuous_on S f" proof - have [simp]: "S \ f -` f ` S = S" by auto show ?thesis - using ope [OF T] - apply (simp add: continuous_on_open) - by (meson ope openin_imp_subset openin_trans) + by (meson T continuous_on_open_gen ope openin_imp_subset) qed lemma quotient_map_imp_continuous_closed: assumes T: "f ` S \ T" and ope: "\U. U \ T \ (closedin (top_of_set S) (S \ f -` U) \ closedin (top_of_set T) U)" shows "continuous_on S f" proof - have [simp]: "S \ f -` f ` S = S" by auto show ?thesis - using ope [OF T] - apply (simp add: continuous_on_closed) - by (metis (no_types, lifting) ope closedin_imp_subset closedin_trans) + by (meson T closedin_imp_subset continuous_on_closed_gen ope) qed lemma open_map_imp_quotient_map: assumes contf: "continuous_on S f" and T: "T \ f ` S" and ope: "\T. openin (top_of_set S) T \ openin (top_of_set (f ` S)) (f ` T)" shows "openin (top_of_set S) (S \ f -` T) = openin (top_of_set (f ` S)) T" proof - have "T = f ` (S \ f -` T)" using T by blast then show ?thesis using "ope" contf continuous_on_open by metis qed lemma closed_map_imp_quotient_map: assumes contf: "continuous_on S f" and T: "T \ f ` S" and ope: "\T. closedin (top_of_set S) T \ closedin (top_of_set (f ` S)) (f ` T)" shows "openin (top_of_set S) (S \ f -` T) \ openin (top_of_set (f ` S)) T" (is "?lhs = ?rhs") proof assume ?lhs then have *: "closedin (top_of_set S) (S - (S \ f -` T))" using closedin_diff by fastforce have [simp]: "(f ` S - f ` (S - (S \ f -` T))) = T" using T by blast show ?rhs using ope [OF *, unfolded closedin_def] by auto next assume ?rhs with contf show ?lhs by (auto simp: continuous_on_open) qed lemma continuous_right_inverse_imp_quotient_map: assumes contf: "continuous_on S f" and imf: "f ` S \ T" and contg: "continuous_on T g" and img: "g ` T \ S" and fg [simp]: "\y. y \ T \ f(g y) = y" and U: "U \ T" shows "openin (top_of_set S) (S \ f -` U) \ openin (top_of_set T) U" (is "?lhs = ?rhs") proof - have f: "\Z. openin (top_of_set (f ` S)) Z \ openin (top_of_set S) (S \ f -` Z)" and g: "\Z. openin (top_of_set (g ` T)) Z \ openin (top_of_set T) (T \ g -` Z)" using contf contg by (auto simp: continuous_on_open) show ?thesis proof have "T \ g -` (g ` T \ (S \ f -` U)) = {x \ T. f (g x) \ U}" using imf img by blast also have "... = U" using U by auto finally have eq: "T \ g -` (g ` T \ (S \ f -` U)) = U" . assume ?lhs then have *: "openin (top_of_set (g ` T)) (g ` T \ (S \ f -` U))" by (meson img openin_Int openin_subtopology_Int_subset openin_subtopology_self) show ?rhs using g [OF *] eq by auto next assume rhs: ?rhs show ?lhs by (metis f fg image_eqI image_subset_iff imf img openin_subopen openin_subtopology_self openin_trans rhs) qed qed lemma continuous_left_inverse_imp_quotient_map: assumes "continuous_on S f" and "continuous_on (f ` S) g" and "\x. x \ S \ g(f x) = x" and "U \ f ` S" shows "openin (top_of_set S) (S \ f -` U) \ openin (top_of_set (f ` S)) U" apply (rule continuous_right_inverse_imp_quotient_map) using assms apply force+ done lemma continuous_imp_quotient_map: fixes f :: "'a::t2_space \ 'b::t2_space" assumes "continuous_on S f" "f ` S = T" "compact S" "U \ T" shows "openin (top_of_set S) (S \ f -` U) \ openin (top_of_set T) U" by (metis (no_types, lifting) assms closed_map_imp_quotient_map continuous_imp_closed_map) subsection\<^marker>\tag unimportant\\Pasting lemmas for functions, for of casewise definitions\ subsubsection\on open sets\ lemma pasting_lemma: assumes ope: "\i. i \ I \ openin X (T i)" and cont: "\i. i \ I \ continuous_map(subtopology X (T i)) Y (f i)" and f: "\i j x. \i \ I; j \ I; x \ topspace X \ T i \ T j\ \ f i x = f j x" and g: "\x. x \ topspace X \ \j. j \ I \ x \ T j \ g x = f j x" shows "continuous_map X Y g" unfolding continuous_map_openin_preimage_eq proof (intro conjI allI impI) show "g ` topspace X \ topspace Y" using g cont continuous_map_image_subset_topspace by fastforce next fix U assume Y: "openin Y U" have T: "T i \ topspace X" if "i \ I" for i using ope by (simp add: openin_subset that) have *: "topspace X \ g -` U = (\i \ I. T i \ f i -` U)" using f g T by fastforce have "\i. i \ I \ openin X (T i \ f i -` U)" using cont unfolding continuous_map_openin_preimage_eq by (metis Y T inf.commute inf_absorb1 ope topspace_subtopology openin_trans_full) then show "openin X (topspace X \ g -` U)" by (auto simp: *) qed lemma pasting_lemma_exists: assumes X: "topspace X \ (\i \ I. T i)" and ope: "\i. i \ I \ openin X (T i)" and cont: "\i. i \ I \ continuous_map (subtopology X (T i)) Y (f i)" and f: "\i j x. \i \ I; j \ I; x \ topspace X \ T i \ T j\ \ f i x = f j x" obtains g where "continuous_map X Y g" "\x i. \i \ I; x \ topspace X \ T i\ \ g x = f i x" proof let ?h = "\x. f (SOME i. i \ I \ x \ T i) x" show "continuous_map X Y ?h" apply (rule pasting_lemma [OF ope cont]) apply (blast intro: f)+ by (metis (no_types, lifting) UN_E X subsetD someI_ex) show "f (SOME i. i \ I \ x \ T i) x = f i x" if "i \ I" "x \ topspace X \ T i" for i x by (metis (no_types, lifting) IntD2 IntI f someI_ex that) qed lemma pasting_lemma_locally_finite: assumes fin: "\x. x \ topspace X \ \V. openin X V \ x \ V \ finite {i \ I. T i \ V \ {}}" and clo: "\i. i \ I \ closedin X (T i)" and cont: "\i. i \ I \ continuous_map(subtopology X (T i)) Y (f i)" and f: "\i j x. \i \ I; j \ I; x \ topspace X \ T i \ T j\ \ f i x = f j x" and g: "\x. x \ topspace X \ \j. j \ I \ x \ T j \ g x = f j x" shows "continuous_map X Y g" unfolding continuous_map_closedin_preimage_eq proof (intro conjI allI impI) show "g ` topspace X \ topspace Y" using g cont continuous_map_image_subset_topspace by fastforce next fix U assume Y: "closedin Y U" have T: "T i \ topspace X" if "i \ I" for i using clo by (simp add: closedin_subset that) have *: "topspace X \ g -` U = (\i \ I. T i \ f i -` U)" using f g T by fastforce have cTf: "\i. i \ I \ closedin X (T i \ f i -` U)" using cont unfolding continuous_map_closedin_preimage_eq topspace_subtopology by (simp add: Int_absorb1 T Y clo closedin_closed_subtopology) have sub: "{Z \ (\i. T i \ f i -` U) ` I. Z \ V \ {}} \ (\i. T i \ f i -` U) ` {i \ I. T i \ V \ {}}" for V by auto have 1: "(\i\I. T i \ f i -` U) \ topspace X" using T by blast then have lf: "locally_finite_in X ((\i. T i \ f i -` U) ` I)" unfolding locally_finite_in_def using finite_subset [OF sub] fin by force show "closedin X (topspace X \ g -` U)" apply (subst *) apply (rule closedin_locally_finite_Union) apply (auto intro: cTf lf) done qed subsubsection\Likewise on closed sets, with a finiteness assumption\ lemma pasting_lemma_closed: assumes fin: "finite I" and clo: "\i. i \ I \ closedin X (T i)" and cont: "\i. i \ I \ continuous_map(subtopology X (T i)) Y (f i)" and f: "\i j x. \i \ I; j \ I; x \ topspace X \ T i \ T j\ \ f i x = f j x" and g: "\x. x \ topspace X \ \j. j \ I \ x \ T j \ g x = f j x" shows "continuous_map X Y g" using pasting_lemma_locally_finite [OF _ clo cont f g] fin by auto lemma pasting_lemma_exists_locally_finite: assumes fin: "\x. x \ topspace X \ \V. openin X V \ x \ V \ finite {i \ I. T i \ V \ {}}" and X: "topspace X \ \(T ` I)" and clo: "\i. i \ I \ closedin X (T i)" and cont: "\i. i \ I \ continuous_map(subtopology X (T i)) Y (f i)" and f: "\i j x. \i \ I; j \ I; x \ topspace X \ T i \ T j\ \ f i x = f j x" and g: "\x. x \ topspace X \ \j. j \ I \ x \ T j \ g x = f j x" obtains g where "continuous_map X Y g" "\x i. \i \ I; x \ topspace X \ T i\ \ g x = f i x" proof show "continuous_map X Y (\x. f(@i. i \ I \ x \ T i) x)" apply (rule pasting_lemma_locally_finite [OF fin]) apply (blast intro: assms)+ by (metis (no_types, lifting) UN_E X set_rev_mp someI_ex) next fix x i assume "i \ I" and "x \ topspace X \ T i" show "f (SOME i. i \ I \ x \ T i) x = f i x" apply (rule someI2_ex) using \i \ I\ \x \ topspace X \ T i\ apply blast by (meson Int_iff \i \ I\ \x \ topspace X \ T i\ f) qed lemma pasting_lemma_exists_closed: assumes fin: "finite I" and X: "topspace X \ \(T ` I)" and clo: "\i. i \ I \ closedin X (T i)" and cont: "\i. i \ I \ continuous_map(subtopology X (T i)) Y (f i)" and f: "\i j x. \i \ I; j \ I; x \ topspace X \ T i \ T j\ \ f i x = f j x" obtains g where "continuous_map X Y g" "\x i. \i \ I; x \ topspace X \ T i\ \ g x = f i x" proof show "continuous_map X Y (\x. f (SOME i. i \ I \ x \ T i) x)" apply (rule pasting_lemma_closed [OF \finite I\ clo cont]) apply (blast intro: f)+ by (metis (mono_tags, lifting) UN_iff X someI_ex subset_iff) next fix x i assume "i \ I" "x \ topspace X \ T i" then show "f (SOME i. i \ I \ x \ T i) x = f i x" by (metis (no_types, lifting) IntD2 IntI f someI_ex) qed lemma continuous_map_cases: assumes f: "continuous_map (subtopology X (X closure_of {x. P x})) Y f" and g: "continuous_map (subtopology X (X closure_of {x. \ P x})) Y g" and fg: "\x. x \ X frontier_of {x. P x} \ f x = g x" shows "continuous_map X Y (\x. if P x then f x else g x)" proof (rule pasting_lemma_closed) let ?f = "\b. if b then f else g" let ?g = "\x. if P x then f x else g x" let ?T = "\b. if b then X closure_of {x. P x} else X closure_of {x. ~P x}" show "finite {True,False}" by auto have eq: "topspace X - Collect P = topspace X \ {x. \ P x}" by blast show "?f i x = ?f j x" if "i \ {True,False}" "j \ {True,False}" and x: "x \ topspace X \ ?T i \ ?T j" for i j x proof - have "f x = g x" if "i" "\ j" apply (rule fg) unfolding frontier_of_closures eq using x that closure_of_restrict by fastforce moreover have "g x = f x" if "x \ X closure_of {x. \ P x}" "x \ X closure_of Collect P" "\ i" "j" for x apply (rule fg [symmetric]) unfolding frontier_of_closures eq using x that closure_of_restrict by fastforce ultimately show ?thesis using that by (auto simp flip: closure_of_restrict) qed show "\j. j \ {True,False} \ x \ ?T j \ (if P x then f x else g x) = ?f j x" if "x \ topspace X" for x apply simp apply safe apply (metis Int_iff closure_of inf_sup_absorb mem_Collect_eq that) by (metis DiffI eq closure_of_subset_Int contra_subsetD mem_Collect_eq that) qed (auto simp: f g) lemma continuous_map_cases_alt: assumes f: "continuous_map (subtopology X (X closure_of {x \ topspace X. P x})) Y f" and g: "continuous_map (subtopology X (X closure_of {x \ topspace X. ~P x})) Y g" and fg: "\x. x \ X frontier_of {x \ topspace X. P x} \ f x = g x" shows "continuous_map X Y (\x. if P x then f x else g x)" apply (rule continuous_map_cases) using assms apply (simp_all add: Collect_conj_eq closure_of_restrict [symmetric] frontier_of_restrict [symmetric]) done lemma continuous_map_cases_function: assumes contp: "continuous_map X Z p" and contf: "continuous_map (subtopology X {x \ topspace X. p x \ Z closure_of U}) Y f" and contg: "continuous_map (subtopology X {x \ topspace X. p x \ Z closure_of (topspace Z - U)}) Y g" and fg: "\x. \x \ topspace X; p x \ Z frontier_of U\ \ f x = g x" shows "continuous_map X Y (\x. if p x \ U then f x else g x)" proof (rule continuous_map_cases_alt) show "continuous_map (subtopology X (X closure_of {x \ topspace X. p x \ U})) Y f" proof (rule continuous_map_from_subtopology_mono) let ?T = "{x \ topspace X. p x \ Z closure_of U}" show "continuous_map (subtopology X ?T) Y f" by (simp add: contf) show "X closure_of {x \ topspace X. p x \ U} \ ?T" by (rule continuous_map_closure_preimage_subset [OF contp]) qed show "continuous_map (subtopology X (X closure_of {x \ topspace X. p x \ U})) Y g" proof (rule continuous_map_from_subtopology_mono) let ?T = "{x \ topspace X. p x \ Z closure_of (topspace Z - U)}" show "continuous_map (subtopology X ?T) Y g" by (simp add: contg) have "X closure_of {x \ topspace X. p x \ U} \ X closure_of {x \ topspace X. p x \ topspace Z - U}" apply (rule closure_of_mono) using continuous_map_closedin contp by fastforce then show "X closure_of {x \ topspace X. p x \ U} \ ?T" by (rule order_trans [OF _ continuous_map_closure_preimage_subset [OF contp]]) qed next show "f x = g x" if "x \ X frontier_of {x \ topspace X. p x \ U}" for x using that continuous_map_frontier_frontier_preimage_subset [OF contp, of U] fg by blast qed subsection \Retractions\ definition\<^marker>\tag important\ retraction :: "('a::topological_space) set \ 'a set \ ('a \ 'a) \ bool" where "retraction S T r \ T \ S \ continuous_on S r \ r ` S \ T \ (\x\T. r x = x)" definition\<^marker>\tag important\ retract_of (infixl "retract'_of" 50) where "T retract_of S \ (\r. retraction S T r)" lemma retraction_idempotent: "retraction S T r \ x \ S \ r (r x) = r x" unfolding retraction_def by auto text \Preservation of fixpoints under (more general notion of) retraction\ lemma invertible_fixpoint_property: fixes S :: "'a::topological_space set" and T :: "'b::topological_space set" assumes contt: "continuous_on T i" and "i ` T \ S" and contr: "continuous_on S r" and "r ` S \ T" and ri: "\y. y \ T \ r (i y) = y" and FP: "\f. \continuous_on S f; f ` S \ S\ \ \x\S. f x = x" and contg: "continuous_on T g" and "g ` T \ T" obtains y where "y \ T" and "g y = y" proof - have "\x\S. (i \ g \ r) x = x" proof (rule FP) show "continuous_on S (i \ g \ r)" by (meson contt contr assms(4) contg assms(8) continuous_on_compose continuous_on_subset) show "(i \ g \ r) ` S \ S" using assms(2,4,8) by force qed then obtain x where x: "x \ S" "(i \ g \ r) x = x" .. then have *: "g (r x) \ T" using assms(4,8) by auto have "r ((i \ g \ r) x) = r x" using x by auto then show ?thesis using "*" ri that by auto qed lemma homeomorphic_fixpoint_property: fixes S :: "'a::topological_space set" and T :: "'b::topological_space set" assumes "S homeomorphic T" shows "(\f. continuous_on S f \ f ` S \ S \ (\x\S. f x = x)) \ (\g. continuous_on T g \ g ` T \ T \ (\y\T. g y = y))" (is "?lhs = ?rhs") proof - obtain r i where r: "\x\S. i (r x) = x" "r ` S = T" "continuous_on S r" "\y\T. r (i y) = y" "i ` T = S" "continuous_on T i" using assms unfolding homeomorphic_def homeomorphism_def by blast show ?thesis proof assume ?lhs with r show ?rhs by (metis invertible_fixpoint_property[of T i S r] order_refl) next assume ?rhs with r show ?lhs by (metis invertible_fixpoint_property[of S r T i] order_refl) qed qed lemma retract_fixpoint_property: fixes f :: "'a::topological_space \ 'b::topological_space" and S :: "'a set" assumes "T retract_of S" and FP: "\f. \continuous_on S f; f ` S \ S\ \ \x\S. f x = x" and contg: "continuous_on T g" and "g ` T \ T" obtains y where "y \ T" and "g y = y" proof - obtain h where "retraction S T h" using assms(1) unfolding retract_of_def .. then show ?thesis unfolding retraction_def using invertible_fixpoint_property[OF continuous_on_id _ _ _ _ FP] by (metis assms(4) contg image_ident that) qed lemma retraction: "retraction S T r \ T \ S \ continuous_on S r \ r ` S = T \ (\x \ T. r x = x)" by (force simp: retraction_def) lemma retractionE: \ \yields properties normalized wrt. simp -- less likely to loop\ assumes "retraction S T r" obtains "T = r ` S" "r ` S \ S" "continuous_on S r" "\x. x \ S \ r (r x) = r x" proof (rule that) from retraction [of S T r] assms have "T \ S" "continuous_on S r" "r ` S = T" and "\x \ T. r x = x" by simp_all then show "T = r ` S" "r ` S \ S" "continuous_on S r" by simp_all from \\x \ T. r x = x\ have "r x = x" if "x \ T" for x using that by simp with \r ` S = T\ show "r (r x) = r x" if "x \ S" for x using that by auto qed lemma retract_ofE: \ \yields properties normalized wrt. simp -- less likely to loop\ assumes "T retract_of S" obtains r where "T = r ` S" "r ` S \ S" "continuous_on S r" "\x. x \ S \ r (r x) = r x" proof - from assms obtain r where "retraction S T r" by (auto simp add: retract_of_def) with that show thesis by (auto elim: retractionE) qed lemma retract_of_imp_extensible: assumes "S retract_of T" and "continuous_on S f" and "f ` S \ U" obtains g where "continuous_on T g" "g ` T \ U" "\x. x \ S \ g x = f x" proof - from \S retract_of T\ obtain r where "retraction T S r" by (auto simp add: retract_of_def) show thesis by (rule that [of "f \ r"]) (use \continuous_on S f\ \f ` S \ U\ \retraction T S r\ in \auto simp: continuous_on_compose2 retraction\) qed lemma idempotent_imp_retraction: assumes "continuous_on S f" and "f ` S \ S" and "\x. x \ S \ f(f x) = f x" shows "retraction S (f ` S) f" by (simp add: assms retraction) lemma retraction_subset: assumes "retraction S T r" and "T \ s'" and "s' \ S" shows "retraction s' T r" unfolding retraction_def by (metis assms continuous_on_subset image_mono retraction) lemma retract_of_subset: assumes "T retract_of S" and "T \ s'" and "s' \ S" shows "T retract_of s'" by (meson assms retract_of_def retraction_subset) lemma retraction_refl [simp]: "retraction S S (\x. x)" by (simp add: retraction) lemma retract_of_refl [iff]: "S retract_of S" unfolding retract_of_def retraction_def using continuous_on_id by blast lemma retract_of_imp_subset: "S retract_of T \ S \ T" by (simp add: retract_of_def retraction_def) lemma retract_of_empty [simp]: "({} retract_of S) \ S = {}" "(S retract_of {}) \ S = {}" by (auto simp: retract_of_def retraction_def) lemma retract_of_singleton [iff]: "({x} retract_of S) \ x \ S" unfolding retract_of_def retraction_def by force lemma retraction_comp: "\retraction S T f; retraction T U g\ \ retraction S U (g \ f)" apply (auto simp: retraction_def intro: continuous_on_compose2) by blast lemma retract_of_trans [trans]: assumes "S retract_of T" and "T retract_of U" shows "S retract_of U" using assms by (auto simp: retract_of_def intro: retraction_comp) lemma closedin_retract: fixes S :: "'a :: t2_space set" assumes "S retract_of T" shows "closedin (top_of_set T) S" proof - obtain r where r: "S \ T" "continuous_on T r" "r ` T \ S" "\x. x \ S \ r x = x" using assms by (auto simp: retract_of_def retraction_def) have "S = {x\T. x = r x}" using r by auto also have "\ = T \ ((\x. (x, r x)) -` ({y. \x. y = (x, x)}))" unfolding vimage_def mem_Times_iff fst_conv snd_conv using r by auto also have "closedin (top_of_set T) \" by (rule continuous_closedin_preimage) (auto intro!: closed_diagonal continuous_on_Pair r) finally show ?thesis . qed lemma closedin_self [simp]: "closedin (top_of_set S) S" by simp lemma retract_of_closed: fixes S :: "'a :: t2_space set" shows "\closed T; S retract_of T\ \ closed S" by (metis closedin_retract closedin_closed_eq) lemma retract_of_compact: "\compact T; S retract_of T\ \ compact S" by (metis compact_continuous_image retract_of_def retraction) lemma retract_of_connected: "\connected T; S retract_of T\ \ connected S" by (metis Topological_Spaces.connected_continuous_image retract_of_def retraction) lemma retraction_openin_vimage_iff: "openin (top_of_set S) (S \ r -` U) \ openin (top_of_set T) U" if retraction: "retraction S T r" and "U \ T" using retraction apply (rule retractionE) apply (rule continuous_right_inverse_imp_quotient_map [where g=r]) using \U \ T\ apply (auto elim: continuous_on_subset) done lemma retract_of_Times: "\S retract_of s'; T retract_of t'\ \ (S \ T) retract_of (s' \ t')" apply (simp add: retract_of_def retraction_def Sigma_mono, clarify) apply (rename_tac f g) apply (rule_tac x="\z. ((f \ fst) z, (g \ snd) z)" in exI) apply (rule conjI continuous_intros | erule continuous_on_subset | force)+ done subsection\Retractions on a topological space\ definition retract_of_space :: "'a set \ 'a topology \ bool" (infix "retract'_of'_space" 50) where "S retract_of_space X \ S \ topspace X \ (\r. continuous_map X (subtopology X S) r \ (\x \ S. r x = x))" lemma retract_of_space_retraction_maps: "S retract_of_space X \ S \ topspace X \ (\r. retraction_maps X (subtopology X S) r id)" by (auto simp: retract_of_space_def retraction_maps_def) lemma retract_of_space_section_map: "S retract_of_space X \ S \ topspace X \ section_map (subtopology X S) X id" unfolding retract_of_space_def retraction_maps_def section_map_def by (auto simp: continuous_map_from_subtopology) lemma retract_of_space_imp_subset: "S retract_of_space X \ S \ topspace X" by (simp add: retract_of_space_def) lemma retract_of_space_topspace: "topspace X retract_of_space X" using retract_of_space_def by force lemma retract_of_space_empty [simp]: "{} retract_of_space X \ topspace X = {}" by (auto simp: continuous_map_def retract_of_space_def) lemma retract_of_space_singleton [simp]: "{a} retract_of_space X \ a \ topspace X" proof - have "continuous_map X (subtopology X {a}) (\x. a) \ (\x. a) a = a" if "a \ topspace X" using that by simp then show ?thesis by (force simp: retract_of_space_def) qed lemma retract_of_space_clopen: assumes "openin X S" "closedin X S" "S = {} \ topspace X = {}" shows "S retract_of_space X" proof (cases "S = {}") case False then obtain a where "a \ S" by blast show ?thesis unfolding retract_of_space_def proof (intro exI conjI) show "S \ topspace X" by (simp add: assms closedin_subset) have "continuous_map X X (\x. if x \ S then x else a)" proof (rule continuous_map_cases) show "continuous_map (subtopology X (X closure_of {x. x \ S})) X (\x. x)" by (simp add: continuous_map_from_subtopology) show "continuous_map (subtopology X (X closure_of {x. x \ S})) X (\x. a)" using \S \ topspace X\ \a \ S\ by force show "x = a" if "x \ X frontier_of {x. x \ S}" for x using assms that clopenin_eq_frontier_of by fastforce qed then show "continuous_map X (subtopology X S) (\x. if x \ S then x else a)" using \S \ topspace X\ \a \ S\ by (auto simp: continuous_map_in_subtopology) qed auto qed (use assms in auto) lemma retract_of_space_disjoint_union: assumes "openin X S" "openin X T" and ST: "disjnt S T" "S \ T = topspace X" and "S = {} \ topspace X = {}" shows "S retract_of_space X" proof (rule retract_of_space_clopen) have "S \ T = {}" by (meson ST disjnt_def) then have "S = topspace X - T" using ST by auto then show "closedin X S" using \openin X T\ by blast qed (auto simp: assms) lemma retraction_maps_section_image1: assumes "retraction_maps X Y r s" shows "s ` (topspace Y) retract_of_space X" unfolding retract_of_space_section_map proof show "s ` topspace Y \ topspace X" using assms continuous_map_image_subset_topspace retraction_maps_def by blast show "section_map (subtopology X (s ` topspace Y)) X id" unfolding section_map_def using assms retraction_maps_to_retract_maps by blast qed lemma retraction_maps_section_image2: "retraction_maps X Y r s \ subtopology X (s ` (topspace Y)) homeomorphic_space Y" using embedding_map_imp_homeomorphic_space homeomorphic_space_sym section_imp_embedding_map section_map_def by blast subsection\Paths and path-connectedness\ definition pathin :: "'a topology \ (real \ 'a) \ bool" where "pathin X g \ continuous_map (subtopology euclideanreal {0..1}) X g" lemma pathin_compose: "\pathin X g; continuous_map X Y f\ \ pathin Y (f \ g)" by (simp add: continuous_map_compose pathin_def) lemma pathin_subtopology: "pathin (subtopology X S) g \ pathin X g \ (\x \ {0..1}. g x \ S)" by (auto simp: pathin_def continuous_map_in_subtopology) lemma pathin_const: "pathin X (\x. a) \ a \ topspace X" by (simp add: pathin_def) lemma path_start_in_topspace: "pathin X g \ g 0 \ topspace X" by (force simp: pathin_def continuous_map) lemma path_finish_in_topspace: "pathin X g \ g 1 \ topspace X" by (force simp: pathin_def continuous_map) lemma path_image_subset_topspace: "pathin X g \ g ` ({0..1}) \ topspace X" by (force simp: pathin_def continuous_map) definition path_connected_space :: "'a topology \ bool" where "path_connected_space X \ \x \ topspace X. \ y \ topspace X. \g. pathin X g \ g 0 = x \ g 1 = y" definition path_connectedin :: "'a topology \ 'a set \ bool" where "path_connectedin X S \ S \ topspace X \ path_connected_space(subtopology X S)" lemma path_connectedin_absolute [simp]: "path_connectedin (subtopology X S) S \ path_connectedin X S" by (simp add: path_connectedin_def subtopology_subtopology) lemma path_connectedin_subset_topspace: "path_connectedin X S \ S \ topspace X" by (simp add: path_connectedin_def) lemma path_connectedin_subtopology: "path_connectedin (subtopology X S) T \ path_connectedin X T \ T \ S" by (auto simp: path_connectedin_def subtopology_subtopology inf.absorb2) lemma path_connectedin: "path_connectedin X S \ S \ topspace X \ (\x \ S. \y \ S. \g. pathin X g \ g ` {0..1} \ S \ g 0 = x \ g 1 = y)" unfolding path_connectedin_def path_connected_space_def pathin_def continuous_map_in_subtopology by (intro conj_cong refl ball_cong) (simp_all add: inf.absorb_iff2) lemma path_connectedin_topspace: "path_connectedin X (topspace X) \ path_connected_space X" by (simp add: path_connectedin_def) lemma path_connected_imp_connected_space: assumes "path_connected_space X" shows "connected_space X" proof - have *: "\S. connectedin X S \ g 0 \ S \ g 1 \ S" if "pathin X g" for g proof (intro exI conjI) have "continuous_map (subtopology euclideanreal {0..1}) X g" using connectedin_absolute that by (simp add: pathin_def) then show "connectedin X (g ` {0..1})" by (rule connectedin_continuous_map_image) auto qed auto show ?thesis using assms by (auto intro: * simp add: path_connected_space_def connected_space_subconnected Ball_def) qed lemma path_connectedin_imp_connectedin: "path_connectedin X S \ connectedin X S" by (simp add: connectedin_def path_connected_imp_connected_space path_connectedin_def) lemma path_connected_space_topspace_empty: "topspace X = {} \ path_connected_space X" by (simp add: path_connected_space_def) lemma path_connectedin_empty [simp]: "path_connectedin X {}" by (simp add: path_connectedin) lemma path_connectedin_singleton [simp]: "path_connectedin X {a} \ a \ topspace X" proof show "path_connectedin X {a} \ a \ topspace X" by (simp add: path_connectedin) show "a \ topspace X \ path_connectedin X {a}" unfolding path_connectedin using pathin_const by fastforce qed lemma path_connectedin_continuous_map_image: assumes f: "continuous_map X Y f" and S: "path_connectedin X S" shows "path_connectedin Y (f ` S)" proof - have fX: "f ` (topspace X) \ topspace Y" by (metis f continuous_map_image_subset_topspace) show ?thesis unfolding path_connectedin proof (intro conjI ballI; clarify?) fix x assume "x \ S" show "f x \ topspace Y" by (meson S fX \x \ S\ image_subset_iff path_connectedin_subset_topspace set_mp) next fix x y assume "x \ S" and "y \ S" then obtain g where g: "pathin X g" "g ` {0..1} \ S" "g 0 = x" "g 1 = y" using S by (force simp: path_connectedin) show "\g. pathin Y g \ g ` {0..1} \ f ` S \ g 0 = f x \ g 1 = f y" proof (intro exI conjI) show "pathin Y (f \ g)" using \pathin X g\ f pathin_compose by auto qed (use g in auto) qed qed lemma path_connectedin_discrete_topology: "path_connectedin (discrete_topology U) S \ S \ U \ (\a. S \ {a})" apply safe using path_connectedin_subset_topspace apply fastforce apply (meson connectedin_discrete_topology path_connectedin_imp_connectedin) using subset_singletonD by fastforce lemma path_connected_space_discrete_topology: "path_connected_space (discrete_topology U) \ (\a. U \ {a})" by (metis path_connectedin_discrete_topology path_connectedin_topspace path_connected_space_topspace_empty subset_singletonD topspace_discrete_topology) lemma homeomorphic_path_connected_space_imp: "\path_connected_space X; X homeomorphic_space Y\ \ path_connected_space Y" unfolding homeomorphic_space_def homeomorphic_maps_def by (metis (no_types, hide_lams) continuous_map_closedin continuous_map_image_subset_topspace imageI order_class.order.antisym path_connectedin_continuous_map_image path_connectedin_topspace subsetI) lemma homeomorphic_path_connected_space: "X homeomorphic_space Y \ path_connected_space X \ path_connected_space Y" by (meson homeomorphic_path_connected_space_imp homeomorphic_space_sym) lemma homeomorphic_map_path_connectedness: assumes "homeomorphic_map X Y f" "U \ topspace X" shows "path_connectedin Y (f ` U) \ path_connectedin X U" unfolding path_connectedin_def proof (intro conj_cong homeomorphic_path_connected_space) show "(f ` U \ topspace Y) = (U \ topspace X)" using assms homeomorphic_imp_surjective_map by blast next assume "U \ topspace X" show "subtopology Y (f ` U) homeomorphic_space subtopology X U" using assms unfolding homeomorphic_eq_everything_map by (metis (no_types, hide_lams) assms homeomorphic_map_subtopologies homeomorphic_space homeomorphic_space_sym image_mono inf.absorb_iff2) qed lemma homeomorphic_map_path_connectedness_eq: "homeomorphic_map X Y f \ path_connectedin X U \ U \ topspace X \ path_connectedin Y (f ` U)" by (meson homeomorphic_map_path_connectedness path_connectedin_def) subsection\Connected components\ definition connected_component_of :: "'a topology \ 'a \ 'a \ bool" where "connected_component_of X x y \ \T. connectedin X T \ x \ T \ y \ T" abbreviation connected_component_of_set where "connected_component_of_set X x \ Collect (connected_component_of X x)" definition connected_components_of :: "'a topology \ ('a set) set" where "connected_components_of X \ connected_component_of_set X ` topspace X" lemma connected_component_in_topspace: "connected_component_of X x y \ x \ topspace X \ y \ topspace X" by (meson connected_component_of_def connectedin_subset_topspace in_mono) lemma connected_component_of_refl: "connected_component_of X x x \ x \ topspace X" by (meson connected_component_in_topspace connected_component_of_def connectedin_sing insertI1) lemma connected_component_of_sym: "connected_component_of X x y \ connected_component_of X y x" by (meson connected_component_of_def) lemma connected_component_of_trans: "\connected_component_of X x y; connected_component_of X y z\ \ connected_component_of X x z" unfolding connected_component_of_def using connectedin_Un by blast lemma connected_component_of_mono: "\connected_component_of (subtopology X S) x y; S \ T\ \ connected_component_of (subtopology X T) x y" by (metis connected_component_of_def connectedin_subtopology inf.absorb_iff2 subtopology_subtopology) lemma connected_component_of_set: "connected_component_of_set X x = {y. \T. connectedin X T \ x \ T \ y \ T}" by (meson connected_component_of_def) lemma connected_component_of_subset_topspace: "connected_component_of_set X x \ topspace X" using connected_component_in_topspace by force lemma connected_component_of_eq_empty: "connected_component_of_set X x = {} \ (x \ topspace X)" using connected_component_in_topspace connected_component_of_refl by fastforce lemma connected_space_iff_connected_component: "connected_space X \ (\x \ topspace X. \y \ topspace X. connected_component_of X x y)" by (simp add: connected_component_of_def connected_space_subconnected) lemma connected_space_imp_connected_component_of: "\connected_space X; a \ topspace X; b \ topspace X\ \ connected_component_of X a b" by (simp add: connected_space_iff_connected_component) lemma connected_space_connected_component_set: "connected_space X \ (\x \ topspace X. connected_component_of_set X x = topspace X)" using connected_component_of_subset_topspace connected_space_iff_connected_component by fastforce lemma connected_component_of_maximal: "\connectedin X S; x \ S\ \ S \ connected_component_of_set X x" by (meson Ball_Collect connected_component_of_def) lemma connected_component_of_equiv: "connected_component_of X x y \ x \ topspace X \ y \ topspace X \ connected_component_of X x = connected_component_of X y" apply (simp add: connected_component_in_topspace fun_eq_iff) by (meson connected_component_of_refl connected_component_of_sym connected_component_of_trans) lemma connected_component_of_disjoint: "disjnt (connected_component_of_set X x) (connected_component_of_set X y) \ ~(connected_component_of X x y)" using connected_component_of_equiv unfolding disjnt_iff by force lemma connected_component_of_eq: "connected_component_of X x = connected_component_of X y \ (x \ topspace X) \ (y \ topspace X) \ x \ topspace X \ y \ topspace X \ connected_component_of X x y" by (metis Collect_empty_eq_bot connected_component_of_eq_empty connected_component_of_equiv) lemma connectedin_connected_component_of: "connectedin X (connected_component_of_set X x)" proof - have "connected_component_of_set X x = \ {T. connectedin X T \ x \ T}" by (auto simp: connected_component_of_def) then show ?thesis apply (rule ssubst) by (blast intro: connectedin_Union) qed lemma Union_connected_components_of: "\(connected_components_of X) = topspace X" unfolding connected_components_of_def apply (rule equalityI) apply (simp add: SUP_least connected_component_of_subset_topspace) using connected_component_of_refl by fastforce lemma connected_components_of_maximal: "\C \ connected_components_of X; connectedin X S; ~disjnt C S\ \ S \ C" unfolding connected_components_of_def disjnt_def apply clarify by (metis Int_emptyI connected_component_of_def connected_component_of_trans mem_Collect_eq) lemma pairwise_disjoint_connected_components_of: "pairwise disjnt (connected_components_of X)" unfolding connected_components_of_def pairwise_def apply clarify by (metis connected_component_of_disjoint connected_component_of_equiv) lemma complement_connected_components_of_Union: "C \ connected_components_of X \ topspace X - C = \ (connected_components_of X - {C})" apply (rule equalityI) using Union_connected_components_of apply fastforce by (metis Diff_cancel Diff_subset Union_connected_components_of cSup_singleton diff_Union_pairwise_disjoint equalityE insert_subsetI pairwise_disjoint_connected_components_of) lemma nonempty_connected_components_of: "C \ connected_components_of X \ C \ {}" unfolding connected_components_of_def by (metis (no_types, lifting) connected_component_of_eq_empty imageE) lemma connected_components_of_subset: "C \ connected_components_of X \ C \ topspace X" using Union_connected_components_of by fastforce lemma connectedin_connected_components_of: assumes "C \ connected_components_of X" shows "connectedin X C" proof - have "C \ connected_component_of_set X ` topspace X" using assms connected_components_of_def by blast then show ?thesis using connectedin_connected_component_of by fastforce qed lemma connected_component_in_connected_components_of: "connected_component_of_set X a \ connected_components_of X \ a \ topspace X" apply (rule iffI) using connected_component_of_eq_empty nonempty_connected_components_of apply fastforce by (simp add: connected_components_of_def) lemma connected_space_iff_components_eq: "connected_space X \ (\C \ connected_components_of X. \C' \ connected_components_of X. C = C')" apply (rule iffI) apply (force simp: connected_components_of_def connected_space_connected_component_set image_iff) by (metis connected_component_in_connected_components_of connected_component_of_refl connected_space_iff_connected_component mem_Collect_eq) lemma connected_components_of_eq_empty: "connected_components_of X = {} \ topspace X = {}" by (simp add: connected_components_of_def) lemma connected_components_of_empty_space: "topspace X = {} \ connected_components_of X = {}" by (simp add: connected_components_of_eq_empty) lemma connected_components_of_subset_sing: "connected_components_of X \ {S} \ connected_space X \ (topspace X = {} \ topspace X = S)" proof (cases "topspace X = {}") case True then show ?thesis by (simp add: connected_components_of_empty_space connected_space_topspace_empty) next case False then show ?thesis by (metis (no_types, hide_lams) Union_connected_components_of ccpo_Sup_singleton connected_components_of_eq_empty connected_space_iff_components_eq insertI1 singletonD subsetI subset_singleton_iff) qed lemma connected_space_iff_components_subset_singleton: "connected_space X \ (\a. connected_components_of X \ {a})" by (simp add: connected_components_of_subset_sing) lemma connected_components_of_eq_singleton: "connected_components_of X = {S} \ connected_space X \ topspace X \ {} \ S = topspace X" by (metis ccpo_Sup_singleton connected_components_of_subset_sing insert_not_empty subset_singleton_iff) lemma connected_components_of_connected_space: "connected_space X \ connected_components_of X = (if topspace X = {} then {} else {topspace X})" by (simp add: connected_components_of_eq_empty connected_components_of_eq_singleton) lemma exists_connected_component_of_superset: assumes "connectedin X S" and ne: "topspace X \ {}" shows "\C. C \ connected_components_of X \ S \ C" proof (cases "S = {}") case True then show ?thesis using ne connected_components_of_def by blast next case False then show ?thesis by (meson all_not_in_conv assms(1) connected_component_in_connected_components_of connected_component_of_maximal connectedin_subset_topspace in_mono) qed lemma closedin_connected_components_of: assumes "C \ connected_components_of X" shows "closedin X C" proof - obtain x where "x \ topspace X" and x: "C = connected_component_of_set X x" using assms by (auto simp: connected_components_of_def) have "connected_component_of_set X x \ topspace X" by (simp add: connected_component_of_subset_topspace) moreover have "X closure_of connected_component_of_set X x \ connected_component_of_set X x" proof (rule connected_component_of_maximal) show "connectedin X (X closure_of connected_component_of_set X x)" by (simp add: connectedin_closure_of connectedin_connected_component_of) show "x \ X closure_of connected_component_of_set X x" by (simp add: \x \ topspace X\ closure_of connected_component_of_refl) qed ultimately show ?thesis using closure_of_subset_eq x by auto qed lemma closedin_connected_component_of: "closedin X (connected_component_of_set X x)" by (metis closedin_connected_components_of closedin_empty connected_component_in_connected_components_of connected_component_of_eq_empty) lemma connected_component_of_eq_overlap: "connected_component_of_set X x = connected_component_of_set X y \ (x \ topspace X) \ (y \ topspace X) \ ~(connected_component_of_set X x \ connected_component_of_set X y = {})" using connected_component_of_equiv by fastforce lemma connected_component_of_nonoverlap: "connected_component_of_set X x \ connected_component_of_set X y = {} \ (x \ topspace X) \ (y \ topspace X) \ ~(connected_component_of_set X x = connected_component_of_set X y)" by (metis connected_component_of_eq_empty connected_component_of_eq_overlap inf.idem) lemma connected_component_of_overlap: "~(connected_component_of_set X x \ connected_component_of_set X y = {}) \ x \ topspace X \ y \ topspace X \ connected_component_of_set X x = connected_component_of_set X y" by (meson connected_component_of_nonoverlap) - end \ No newline at end of file diff --git a/src/HOL/Analysis/Elementary_Metric_Spaces.thy b/src/HOL/Analysis/Elementary_Metric_Spaces.thy --- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy +++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy @@ -1,3311 +1,3266 @@ (* Author: L C Paulson, University of Cambridge Author: Amine Chaieb, University of Cambridge Author: Robert Himmelmann, TU Muenchen Author: Brian Huffman, Portland State University *) section \Elementary Metric Spaces\ theory Elementary_Metric_Spaces imports Abstract_Topology_2 Metric_Arith begin subsection \Open and closed balls\ definition\<^marker>\tag important\ ball :: "'a::metric_space \ real \ 'a set" where "ball x e = {y. dist x y < e}" definition\<^marker>\tag important\ cball :: "'a::metric_space \ real \ 'a set" where "cball x e = {y. dist x y \ e}" definition\<^marker>\tag important\ sphere :: "'a::metric_space \ real \ 'a set" where "sphere x e = {y. dist x y = e}" lemma mem_ball [simp, metric_unfold]: "y \ ball x e \ dist x y < e" by (simp add: ball_def) lemma mem_cball [simp, metric_unfold]: "y \ cball x e \ dist x y \ e" by (simp add: cball_def) lemma mem_sphere [simp]: "y \ sphere x e \ dist x y = e" by (simp add: sphere_def) lemma ball_trivial [simp]: "ball x 0 = {}" by (simp add: ball_def) lemma cball_trivial [simp]: "cball x 0 = {x}" by (simp add: cball_def) lemma sphere_trivial [simp]: "sphere x 0 = {x}" by (simp add: sphere_def) lemma disjoint_ballI: "dist x y \ r+s \ ball x r \ ball y s = {}" using dist_triangle_less_add not_le by fastforce lemma disjoint_cballI: "dist x y > r + s \ cball x r \ cball y s = {}" by (metis add_mono disjoint_iff_not_equal dist_triangle2 dual_order.trans leD mem_cball) lemma sphere_empty [simp]: "r < 0 \ sphere a r = {}" for a :: "'a::metric_space" by auto lemma centre_in_ball [simp]: "x \ ball x e \ 0 < e" by simp lemma centre_in_cball [simp]: "x \ cball x e \ 0 \ e" by simp lemma ball_subset_cball [simp, intro]: "ball x e \ cball x e" by (simp add: subset_eq) lemma mem_ball_imp_mem_cball: "x \ ball y e \ x \ cball y e" by (auto) lemma sphere_cball [simp,intro]: "sphere z r \ cball z r" by force lemma cball_diff_sphere: "cball a r - sphere a r = ball a r" by auto lemma subset_ball[intro]: "d \ e \ ball x d \ ball x e" by (simp add: subset_eq) lemma subset_cball[intro]: "d \ e \ cball x d \ cball x e" by (simp add: subset_eq) lemma mem_ball_leI: "x \ ball y e \ e \ f \ x \ ball y f" by (auto) lemma mem_cball_leI: "x \ cball y e \ e \ f \ x \ cball y f" by (auto) lemma cball_trans: "y \ cball z b \ x \ cball y a \ x \ cball z (b + a)" by metric lemma ball_max_Un: "ball a (max r s) = ball a r \ ball a s" by (simp add: set_eq_iff) arith lemma ball_min_Int: "ball a (min r s) = ball a r \ ball a s" by (simp add: set_eq_iff) lemma cball_max_Un: "cball a (max r s) = cball a r \ cball a s" by (simp add: set_eq_iff) arith lemma cball_min_Int: "cball a (min r s) = cball a r \ cball a s" by (simp add: set_eq_iff) lemma cball_diff_eq_sphere: "cball a r - ball a r = sphere a r" by (auto simp: cball_def ball_def dist_commute) lemma open_ball [intro, simp]: "open (ball x e)" proof - have "open (dist x -` {.. (\x\S. \e>0. ball x e \ S)" by (simp add: open_dist subset_eq Ball_def dist_commute) lemma openI [intro?]: "(\x. x\S \ \e>0. ball x e \ S) \ open S" by (auto simp: open_contains_ball) lemma openE[elim?]: assumes "open S" "x\S" obtains e where "e>0" "ball x e \ S" using assms unfolding open_contains_ball by auto lemma open_contains_ball_eq: "open S \ x\S \ (\e>0. ball x e \ S)" by (metis open_contains_ball subset_eq centre_in_ball) lemma ball_eq_empty[simp]: "ball x e = {} \ e \ 0" unfolding mem_ball set_eq_iff by (simp add: not_less) metric lemma ball_empty: "e \ 0 \ ball x e = {}" by simp lemma closed_cball [iff]: "closed (cball x e)" proof - have "closed (dist x -` {..e})" by (intro closed_vimage closed_atMost continuous_intros) also have "dist x -` {..e} = cball x e" by auto finally show ?thesis . qed lemma open_contains_cball: "open S \ (\x\S. \e>0. cball x e \ S)" proof - { fix x and e::real assume "x\S" "e>0" "ball x e \ S" then have "\d>0. cball x d \ S" unfolding subset_eq by (rule_tac x="e/2" in exI, auto) } moreover { fix x and e::real assume "x\S" "e>0" "cball x e \ S" then have "\d>0. ball x d \ S" unfolding subset_eq apply (rule_tac x="e/2" in exI, auto) done } ultimately show ?thesis unfolding open_contains_ball by auto qed lemma open_contains_cball_eq: "open S \ (\x. x \ S \ (\e>0. cball x e \ S))" by (metis open_contains_cball subset_eq order_less_imp_le centre_in_cball) lemma eventually_nhds_ball: "d > 0 \ eventually (\x. x \ ball z d) (nhds z)" by (rule eventually_nhds_in_open) simp_all lemma eventually_at_ball: "d > 0 \ eventually (\t. t \ ball z d \ t \ A) (at z within A)" unfolding eventually_at by (intro exI[of _ d]) (simp_all add: dist_commute) lemma eventually_at_ball': "d > 0 \ eventually (\t. t \ ball z d \ t \ z \ t \ A) (at z within A)" unfolding eventually_at by (intro exI[of _ d]) (simp_all add: dist_commute) lemma at_within_ball: "e > 0 \ dist x y < e \ at y within ball x e = at y" by (subst at_within_open) auto lemma atLeastAtMost_eq_cball: fixes a b::real shows "{a .. b} = cball ((a + b)/2) ((b - a)/2)" by (auto simp: dist_real_def field_simps) lemma cball_eq_atLeastAtMost: fixes a b::real shows "cball a b = {a - b .. a + b}" by (auto simp: dist_real_def) lemma greaterThanLessThan_eq_ball: fixes a b::real shows "{a <..< b} = ball ((a + b)/2) ((b - a)/2)" by (auto simp: dist_real_def field_simps) lemma ball_eq_greaterThanLessThan: fixes a b::real shows "ball a b = {a - b <..< a + b}" by (auto simp: dist_real_def) lemma interior_ball [simp]: "interior (ball x e) = ball x e" by (simp add: interior_open) lemma cball_eq_empty [simp]: "cball x e = {} \ 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 \ cball x e = {}" by simp lemma cball_sing: fixes x :: "'a::metric_space" shows "e = 0 \ cball x e = {x}" by (auto simp: set_eq_iff) lemma ball_divide_subset: "d \ 1 \ ball x (e/d) \ ball x e" apply (cases "e \ 0") apply (simp add: ball_empty field_split_simps) apply (rule subset_ball) apply (simp add: field_split_simps) done lemma ball_divide_subset_numeral: "ball x (e / numeral w) \ ball x e" using ball_divide_subset one_le_numeral by blast lemma cball_divide_subset: "d \ 1 \ cball x (e/d) \ cball x e" apply (cases "e < 0") apply (simp add: field_split_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) \ cball x e" using cball_divide_subset one_le_numeral by blast lemma cball_scale: assumes "a \ 0" shows "(\x. a *\<^sub>R x) ` cball c r = cball (a *\<^sub>R c :: 'a :: real_normed_vector) (\a\ * r)" proof - have 1: "(\x. a *\<^sub>R x) ` cball c r \ cball (a *\<^sub>R c) (\a\ * r)" if "a \ 0" for a r and c :: 'a proof safe fix x assume x: "x \ cball c r" have "dist (a *\<^sub>R c) (a *\<^sub>R x) = norm (a *\<^sub>R c - a *\<^sub>R x)" by (auto simp: dist_norm) also have "a *\<^sub>R c - a *\<^sub>R x = a *\<^sub>R (c - x)" by (simp add: algebra_simps) finally show "a *\<^sub>R x \ cball (a *\<^sub>R c) (\a\ * r)" using that x by (auto simp: dist_norm) qed have "cball (a *\<^sub>R c) (\a\ * r) = (\x. a *\<^sub>R x) ` (\x. inverse a *\<^sub>R x) ` cball (a *\<^sub>R c) (\a\ * r)" unfolding image_image using assms by simp also have "\ \ (\x. a *\<^sub>R x) ` cball (inverse a *\<^sub>R (a *\<^sub>R c)) (\inverse a\ * (\a\ * r))" using assms by (intro image_mono 1) auto also have "\ = (\x. a *\<^sub>R x) ` cball c r" using assms by (simp add: algebra_simps) finally have "cball (a *\<^sub>R c) (\a\ * r) \ (\x. a *\<^sub>R x) ` cball c r" . moreover from assms have "(\x. a *\<^sub>R x) ` cball c r \ cball (a *\<^sub>R c) (\a\ * r)" by (intro 1) auto ultimately show ?thesis by blast qed lemma ball_scale: assumes "a \ 0" shows "(\x. a *\<^sub>R x) ` ball c r = ball (a *\<^sub>R c :: 'a :: real_normed_vector) (\a\ * r)" proof - have 1: "(\x. a *\<^sub>R x) ` ball c r \ ball (a *\<^sub>R c) (\a\ * r)" if "a \ 0" for a r and c :: 'a proof safe fix x assume x: "x \ ball c r" have "dist (a *\<^sub>R c) (a *\<^sub>R x) = norm (a *\<^sub>R c - a *\<^sub>R x)" by (auto simp: dist_norm) also have "a *\<^sub>R c - a *\<^sub>R x = a *\<^sub>R (c - x)" by (simp add: algebra_simps) finally show "a *\<^sub>R x \ ball (a *\<^sub>R c) (\a\ * r)" using that x by (auto simp: dist_norm) qed have "ball (a *\<^sub>R c) (\a\ * r) = (\x. a *\<^sub>R x) ` (\x. inverse a *\<^sub>R x) ` ball (a *\<^sub>R c) (\a\ * r)" unfolding image_image using assms by simp also have "\ \ (\x. a *\<^sub>R x) ` ball (inverse a *\<^sub>R (a *\<^sub>R c)) (\inverse a\ * (\a\ * r))" using assms by (intro image_mono 1) auto also have "\ = (\x. a *\<^sub>R x) ` ball c r" using assms by (simp add: algebra_simps) finally have "ball (a *\<^sub>R c) (\a\ * r) \ (\x. a *\<^sub>R x) ` ball c r" . moreover from assms have "(\x. a *\<^sub>R x) ` ball c r \ ball (a *\<^sub>R c) (\a\ * r)" by (intro 1) auto ultimately show ?thesis by blast qed subsection \Limit Points\ lemma islimpt_approachable: fixes x :: "'a::metric_space" shows "x islimpt S \ (\e>0. \x'\S. x' \ x \ dist x' x < e)" unfolding islimpt_iff_eventually eventually_at by fast lemma islimpt_approachable_le: "x islimpt S \ (\e>0. \x'\ S. x' \ x \ dist x' x \ e)" for x :: "'a::metric_space" unfolding islimpt_approachable - using approachable_lt_le [where f="\y. dist y x" and P="\y. y \ S \ y = x", - THEN arg_cong [where f=Not]] - by (simp add: Bex_def conj_commute conj_left_commute) + using approachable_lt_le2 [where f="\y. dist y x" and P="\y. y \ S \ y = x" and Q="\x. True"] + by auto lemma limpt_of_limpts: "x islimpt {y. y islimpt S} \ x islimpt S" for x :: "'a::metric_space" apply (clarsimp simp add: islimpt_approachable) apply (drule_tac x="e/2" in spec) apply (auto simp: simp del: less_divide_eq_numeral1) apply (drule_tac x="dist x' x" in spec) apply (auto simp del: less_divide_eq_numeral1) apply metric done lemma closed_limpts: "closed {x::'a::metric_space. x islimpt S}" using closed_limpt limpt_of_limpts by blast lemma limpt_of_closure: "x islimpt closure S \ x islimpt S" for x :: "'a::metric_space" by (auto simp: closure_def islimpt_Un dest: limpt_of_limpts) lemma islimpt_eq_infinite_ball: "x islimpt S \ (\e>0. infinite(S \ ball x e))" apply (simp add: islimpt_eq_acc_point, safe) apply (metis Int_commute open_ball centre_in_ball) by (metis open_contains_ball Int_mono finite_subset inf_commute subset_refl) lemma islimpt_eq_infinite_cball: "x islimpt S \ (\e>0. infinite(S \ cball x e))" apply (simp add: islimpt_eq_infinite_ball, safe) apply (meson Int_mono ball_subset_cball finite_subset order_refl) by (metis open_ball centre_in_ball finite_Int inf.absorb_iff2 inf_assoc open_contains_cball_eq) subsection \Perfect Metric Spaces\ lemma perfect_choose_dist: "0 < r \ \a. a \ x \ 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} \ e = 0" proof (rule linorder_cases) assume e: "0 < e" obtain a where "a \ x" "dist a x < e" using perfect_choose_dist [OF e] by auto then have "a \ x" "dist x a \ e" by (auto simp: dist_commute) with e show ?thesis by (auto simp: set_eq_iff) qed auto subsection \?\ lemma finite_ball_include: fixes a :: "'a::metric_space" assumes "finite S" shows "\e>0. S \ ball a e" using assms proof induction case (insert x S) then obtain e0 where "e0>0" and e0:"S \ ball a e0" by auto define e where "e = max e0 (2 * dist a x)" have "e>0" unfolding e_def using \e0>0\ by auto moreover have "insert x S \ ball a e" using e0 \e>0\ unfolding e_def by auto ultimately show ?case by auto qed (auto intro: zero_less_one) lemma finite_set_avoid: fixes a :: "'a::metric_space" assumes "finite S" shows "\d>0. \x\S. x \ a \ d \ dist a x" using assms proof induction case (insert x S) then obtain d where "d > 0" and d: "\x\S. x \ a \ d \ dist a x" by blast show ?case proof (cases "x = a") case True with \d > 0 \d show ?thesis by auto next case False let ?d = "min d (dist a x)" from False \d > 0\ have dp: "?d > 0" by auto from d have d': "\x\S. x \ a \ ?d \ dist a x" by auto with dp False show ?thesis by (metis insert_iff le_less min_less_iff_conj not_less) qed qed (auto intro: zero_less_one) lemma discrete_imp_closed: fixes S :: "'a::metric_space set" assumes e: "0 < e" and d: "\x \ S. \y \ S. dist y x < e \ y = x" shows "closed S" proof - have False if C: "\e. e>0 \ \x'\S. x' \ x \ dist x' x < e" for x proof - from e have e2: "e/2 > 0" by arith from C[rule_format, OF e2] obtain y where y: "y \ S" "y \ x" "dist y x < e/2" by blast from e2 y(2) have mp: "min (e/2) (dist x y) > 0" by simp from d y C[OF mp] show ?thesis by metric qed then show ?thesis by (metis islimpt_approachable closed_limpt [where 'a='a]) qed subsection \Interior\ lemma mem_interior: "x \ interior S \ (\e>0. ball x e \ S)" using open_contains_ball_eq [where S="interior S"] by (simp add: open_subset_interior) lemma mem_interior_cball: "x \ interior S \ (\e>0. cball x e \ S)" by (meson ball_subset_cball interior_subset mem_interior open_contains_cball open_interior subset_trans) subsection \Frontier\ lemma frontier_straddle: fixes a :: "'a::metric_space" shows "a \ frontier S \ (\e>0. (\x\S. dist a x < e) \ (\x. x \ S \ dist a x < e))" unfolding frontier_def closure_interior by (auto simp: mem_interior subset_eq ball_def) subsection \Limits\ proposition Lim: "(f \ l) net \ trivial_limit net \ (\e>0. eventually (\x. dist (f x) l < e) net)" by (auto simp: tendsto_iff trivial_limit_eq) text \Show that they yield usual definitions in the various cases.\ proposition Lim_within_le: "(f \ l)(at a within S) \ (\e>0. \d>0. \x\S. 0 < dist x a \ dist x a \ d \ dist (f x) l < e)" by (auto simp: tendsto_iff eventually_at_le) proposition Lim_within: "(f \ l) (at a within S) \ (\e >0. \d>0. \x \ S. 0 < dist x a \ dist x a < d \ dist (f x) l < e)" by (auto simp: tendsto_iff eventually_at) corollary Lim_withinI [intro?]: assumes "\e. e > 0 \ \d>0. \x \ S. 0 < dist x a \ dist x a < d \ dist (f x) l \ e" shows "(f \ l) (at a within S)" apply (simp add: Lim_within, clarify) apply (rule ex_forward [OF assms [OF half_gt_zero]], auto) done proposition Lim_at: "(f \ l) (at a) \ (\e >0. \d>0. \x. 0 < dist x a \ dist x a < d \ dist (f x) l < e)" by (auto simp: tendsto_iff eventually_at) lemma Lim_transform_within_set: fixes a :: "'a::metric_space" and l :: "'b::metric_space" shows "\(f \ l) (at a within S); eventually (\x. x \ S \ x \ T) (at a)\ \ (f \ l) (at a within T)" apply (clarsimp simp: eventually_at Lim_within) apply (drule_tac x=e in spec, clarify) apply (rename_tac k) apply (rule_tac x="min d k" in exI, simp) done text \Another limit point characterization.\ lemma limpt_sequential_inj: fixes x :: "'a::metric_space" shows "x islimpt S \ (\f. (\n::nat. f n \ S - {x}) \ inj f \ (f \ x) sequentially)" (is "?lhs = ?rhs") proof assume ?lhs then have "\e>0. \x'\S. x' \ x \ dist x' x < e" by (force simp: islimpt_approachable) then obtain y where y: "\e. e>0 \ y e \ S \ y e \ x \ dist (y e) x < e" by metis define f where "f \ rec_nat (y 1) (\n fn. y (min (inverse(2 ^ (Suc n))) (dist fn x)))" have [simp]: "f 0 = y 1" "f(Suc n) = y (min (inverse(2 ^ (Suc n))) (dist (f n) x))" for n by (simp_all add: f_def) have f: "f n \ S \ (f n \ x) \ dist (f n) x < inverse(2 ^ n)" for n proof (induction n) case 0 show ?case by (simp add: y) next case (Suc n) then show ?case apply (auto simp: y) by (metis half_gt_zero_iff inverse_positive_iff_positive less_divide_eq_numeral1(1) min_less_iff_conj y zero_less_dist_iff zero_less_numeral zero_less_power) qed show ?rhs proof (rule_tac x=f in exI, intro conjI allI) show "\n. f n \ S - {x}" using f by blast have "dist (f n) x < dist (f m) x" if "m < n" for m n using that proof (induction n) case 0 then show ?case by simp next case (Suc n) then consider "m < n" | "m = n" using less_Suc_eq by blast then show ?case proof cases assume "m < n" have "dist (f(Suc n)) x = dist (y (min (inverse(2 ^ (Suc n))) (dist (f n) x))) x" by simp also have "\ < dist (f n) x" by (metis dist_pos_lt f min.strict_order_iff min_less_iff_conj y) also have "\ < dist (f m) x" using Suc.IH \m < n\ by blast finally show ?thesis . next assume "m = n" then show ?case by simp (metis dist_pos_lt f half_gt_zero_iff inverse_positive_iff_positive min_less_iff_conj y zero_less_numeral zero_less_power) qed qed then show "inj f" by (metis less_irrefl linorder_injI) show "f \ x" apply (rule tendstoI) apply (rule_tac c="nat (ceiling(1/e))" in eventually_sequentiallyI) apply (rule less_trans [OF f [THEN conjunct2, THEN conjunct2]]) apply (simp add: field_simps) by (meson le_less_trans mult_less_cancel_left not_le of_nat_less_two_power) qed next assume ?rhs then show ?lhs by (fastforce simp add: islimpt_approachable lim_sequentially) qed lemma Lim_dist_ubound: assumes "\(trivial_limit net)" and "(f \ l) net" and "eventually (\x. dist a (f x) \ e) net" shows "dist a l \ e" using assms by (fast intro: tendsto_le tendsto_intros) subsection \Continuity\ text\Derive the epsilon-delta forms, which we often use as "definitions"\ proposition continuous_within_eps_delta: "continuous (at x within s) f \ (\e>0. \d>0. \x'\ s. dist x' x < d --> dist (f x') (f x) < e)" unfolding continuous_within and Lim_within by fastforce corollary continuous_at_eps_delta: "continuous (at x) f \ (\e > 0. \d > 0. \x'. dist x' x < d \ dist (f x') (f x) < e)" using continuous_within_eps_delta [of x UNIV f] by simp lemma continuous_at_right_real_increasing: fixes f :: "real \ real" assumes nondecF: "\x y. x \ y \ f x \ f y" shows "continuous (at_right a) f \ (\e>0. \d>0. f (a + d) - f a < e)" apply (simp add: greaterThan_def dist_real_def continuous_within Lim_within_le) apply (intro all_cong ex_cong, safe) apply (erule_tac x="a + d" in allE, simp) apply (simp add: nondecF field_simps) apply (drule nondecF, simp) done lemma continuous_at_left_real_increasing: assumes nondecF: "\ x y. x \ y \ f x \ ((f y) :: real)" shows "(continuous (at_left (a :: real)) f) = (\e > 0. \delta > 0. f a - f (a - delta) < e)" apply (simp add: lessThan_def dist_real_def continuous_within Lim_within_le) apply (intro all_cong ex_cong, safe) apply (erule_tac x="a - d" in allE, simp) apply (simp add: nondecF field_simps) apply (cut_tac x="a - d" and y=x in nondecF, simp_all) done text\Versions in terms of open balls.\ lemma continuous_within_ball: "continuous (at x within s) f \ (\e > 0. \d > 0. f ` (ball x d \ s) \ ball (f x) e)" (is "?lhs = ?rhs") proof assume ?lhs { fix e :: real assume "e > 0" then obtain d where d: "d>0" "\xa\s. 0 < dist xa x \ dist xa x < d \ dist (f xa) (f x) < e" using \?lhs\[unfolded continuous_within Lim_within] by auto { fix y assume "y \ f ` (ball x d \ s)" then have "y \ ball (f x) e" using d(2) using \e > 0\ by (auto simp: dist_commute) } then have "\d>0. f ` (ball x d \ s) \ ball (f x) e" using \d > 0\ unfolding subset_eq ball_def by (auto simp: dist_commute) } then show ?rhs by auto next assume ?rhs then show ?lhs unfolding continuous_within Lim_within ball_def subset_eq apply (auto simp: dist_commute) apply (erule_tac x=e in allE, auto) done qed lemma continuous_at_ball: "continuous (at x) f \ (\e>0. \d>0. f ` (ball x d) \ ball (f x) e)" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs unfolding continuous_at Lim_at subset_eq Ball_def Bex_def image_iff mem_ball - apply auto - apply (erule_tac x=e in allE, auto) - apply (rule_tac x=d in exI, auto) - apply (erule_tac x=xa in allE) - apply (auto simp: dist_commute) - done + by (metis dist_commute dist_pos_lt dist_self) next assume ?rhs then show ?lhs unfolding continuous_at Lim_at subset_eq Ball_def Bex_def image_iff mem_ball - apply auto - apply (erule_tac x=e in allE, auto) - apply (rule_tac x=d in exI, auto) - apply (erule_tac x="f xa" in allE) - apply (auto simp: dist_commute) - done + by (metis dist_commute) qed text\Define setwise continuity in terms of limits within the set.\ lemma continuous_on_iff: "continuous_on s f \ (\x\s. \e>0. \d>0. \x'\s. dist x' x < d \ dist (f x') (f x) < e)" unfolding continuous_on_def Lim_within by (metis dist_pos_lt dist_self) lemma continuous_within_E: assumes "continuous (at x within s) f" "e>0" obtains d where "d>0" "\x'. \x'\ s; dist x' x \ d\ \ dist (f x') (f x) < e" using assms apply (simp add: continuous_within_eps_delta) apply (drule spec [of _ e], clarify) apply (rule_tac d="d/2" in that, auto) done lemma continuous_onI [intro?]: assumes "\x e. \e > 0; x \ s\ \ \d>0. \x'\s. dist x' x < d \ dist (f x') (f x) \ e" shows "continuous_on s f" apply (simp add: continuous_on_iff, clarify) apply (rule ex_forward [OF assms [OF half_gt_zero]], auto) done text\Some simple consequential lemmas.\ lemma continuous_onE: assumes "continuous_on s f" "x\s" "e>0" obtains d where "d>0" "\x'. \x' \ s; dist x' x \ d\ \ dist (f x') (f x) < e" using assms apply (simp add: continuous_on_iff) apply (elim ballE allE) apply (auto intro: that [where d="d/2" for d]) done text\The usual transformation theorems.\ lemma continuous_transform_within: fixes f g :: "'a::metric_space \ 'b::topological_space" assumes "continuous (at x within s) f" and "0 < d" and "x \ s" and "\x'. \x' \ s; dist x' x < d\ \ f x' = g x'" shows "continuous (at x within s) g" using assms unfolding continuous_within by (force intro: Lim_transform_within) subsection \Closure and Limit Characterization\ lemma closure_approachable: fixes S :: "'a::metric_space set" shows "x \ closure S \ (\e>0. \y\S. dist y x < e)" apply (auto simp: closure_def islimpt_approachable) apply (metis dist_self) done lemma closure_approachable_le: fixes S :: "'a::metric_space set" shows "x \ closure S \ (\e>0. \y\S. dist y x \ e)" unfolding closure_approachable using dense by force lemma closure_approachableD: assumes "x \ closure S" "e>0" shows "\y\S. dist x y < e" using assms unfolding closure_approachable by (auto simp: dist_commute) lemma closed_approachable: fixes S :: "'a::metric_space set" shows "closed S \ (\e>0. \y\S. dist y x < e) \ x \ S" by (metis closure_closed closure_approachable) lemma closure_contains_Inf: fixes S :: "real set" assumes "S \ {}" "bdd_below S" shows "Inf S \ closure S" proof - have *: "\x\S. Inf S \ x" using cInf_lower[of _ S] assms by metis { fix e :: real assume "e > 0" then have "Inf S < Inf S + e" by simp with assms obtain x where "x \ S" "x < Inf S + e" by (subst (asm) cInf_less_iff) auto with * have "\x\S. dist x (Inf S) < e" by (intro bexI[of _ x]) (auto simp: dist_real_def) } then show ?thesis unfolding closure_approachable by auto qed lemma closure_contains_Sup: fixes S :: "real set" assumes "S \ {}" "bdd_above S" shows "Sup S \ closure S" proof - have *: "\x\S. x \ Sup S" using cSup_upper[of _ S] assms by metis { fix e :: real assume "e > 0" then have "Sup S - e < Sup S" by simp with assms obtain x where "x \ S" "Sup S - e < x" by (subst (asm) less_cSup_iff) auto with * have "\x\S. dist x (Sup S) < e" by (intro bexI[of _ x]) (auto simp: dist_real_def) } then show ?thesis unfolding closure_approachable by auto qed lemma not_trivial_limit_within_ball: "\ trivial_limit (at x within S) \ (\e>0. S \ ball x e - {x} \ {})" (is "?lhs \ ?rhs") proof show ?rhs if ?lhs proof - { fix e :: real assume "e > 0" then obtain y where "y \ S - {x}" and "dist y x < e" using \?lhs\ not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"] by auto then have "y \ S \ ball x e - {x}" unfolding ball_def by (simp add: dist_commute) then have "S \ ball x e - {x} \ {}" by blast } then show ?thesis by auto qed show ?lhs if ?rhs proof - { fix e :: real assume "e > 0" then obtain y where "y \ S \ ball x e - {x}" using \?rhs\ by blast then have "y \ S - {x}" and "dist y x < e" unfolding ball_def by (simp_all add: dist_commute) then have "\y \ S - {x}. dist y x < e" by auto } then show ?thesis using not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"] by auto qed qed subsection \Boundedness\ (* FIXME: This has to be unified with BSEQ!! *) definition\<^marker>\tag important\ (in metric_space) bounded :: "'a set \ bool" where "bounded S \ (\x e. \y\S. dist x y \ e)" lemma bounded_subset_cball: "bounded S \ (\e x. S \ cball x e \ 0 \ e)" unfolding bounded_def subset_eq by auto (meson order_trans zero_le_dist) lemma bounded_any_center: "bounded S \ (\e. \y\S. dist a y \ e)" unfolding bounded_def by auto (metis add.commute add_le_cancel_right dist_commute dist_triangle_le) lemma bounded_iff: "bounded S \ (\a. \x\S. norm x \ a)" unfolding bounded_any_center [where a=0] by (simp add: dist_norm) lemma bdd_above_norm: "bdd_above (norm ` X) \ bounded X" by (simp add: bounded_iff bdd_above_def) lemma bounded_norm_comp: "bounded ((\x. norm (f x)) ` S) = bounded (f ` S)" by (simp add: bounded_iff) lemma boundedI: assumes "\x. x \ S \ norm x \ B" shows "bounded S" using assms bounded_iff by blast lemma bounded_empty [simp]: "bounded {}" by (simp add: bounded_def) lemma bounded_subset: "bounded T \ S \ T \ bounded S" by (metis bounded_def subset_eq) lemma bounded_interior[intro]: "bounded S \ bounded(interior S)" by (metis bounded_subset interior_subset) lemma bounded_closure[intro]: assumes "bounded S" shows "bounded (closure S)" proof - from assms obtain x and a where a: "\y\S. dist x y \ a" unfolding bounded_def by auto { fix y assume "y \ closure S" then obtain f where f: "\n. f n \ S" "(f \ y) sequentially" unfolding closure_sequential by auto have "\n. f n \ S \ dist x (f n) \ a" using a by simp then have "eventually (\n. dist x (f n) \ a) sequentially" by (simp add: f(1)) - have "dist x y \ a" - apply (rule Lim_dist_ubound [of sequentially f]) - apply (rule trivial_limit_sequentially) - apply (rule f(2)) - apply fact - done + then have "dist x y \ a" + using Lim_dist_ubound f(2) trivial_limit_sequentially by blast } then show ?thesis unfolding bounded_def by auto qed lemma bounded_closure_image: "bounded (f ` closure S) \ bounded (f ` S)" by (simp add: bounded_subset closure_subset image_mono) lemma bounded_cball[simp,intro]: "bounded (cball x e)" - apply (simp add: bounded_def) - apply (rule_tac x=x in exI) - apply (rule_tac x=e in exI, auto) - done + unfolding bounded_def using mem_cball by blast lemma bounded_ball[simp,intro]: "bounded (ball x e)" by (metis ball_subset_cball bounded_cball bounded_subset) lemma bounded_Un[simp]: "bounded (S \ T) \ bounded S \ bounded T" by (auto simp: bounded_def) (metis Un_iff bounded_any_center le_max_iff_disj) lemma bounded_Union[intro]: "finite F \ \S\F. bounded S \ bounded (\F)" by (induct rule: finite_induct[of F]) auto lemma bounded_UN [intro]: "finite A \ \x\A. bounded (B x) \ bounded (\x\A. B x)" - by (induct set: finite) auto + by auto lemma bounded_insert [simp]: "bounded (insert x S) \ bounded S" proof - have "\y\{x}. dist x y \ 0" by simp then have "bounded {x}" unfolding bounded_def by fast then show ?thesis by (metis insert_is_Un bounded_Un) qed lemma bounded_subset_ballI: "S \ ball x r \ bounded S" by (meson bounded_ball bounded_subset) lemma bounded_subset_ballD: assumes "bounded S" shows "\r. 0 < r \ S \ ball x r" proof - obtain e::real and y where "S \ cball y e" "0 \ e" using assms by (auto simp: bounded_subset_cball) then show ?thesis by (intro exI[where x="dist x y + e + 1"]) metric qed lemma finite_imp_bounded [intro]: "finite S \ bounded S" by (induct set: finite) simp_all lemma bounded_Int[intro]: "bounded S \ bounded T \ bounded (S \ T)" by (metis Int_lower1 Int_lower2 bounded_subset) lemma bounded_diff[intro]: "bounded S \ bounded (S - T)" by (metis Diff_subset bounded_subset) lemma bounded_dist_comp: assumes "bounded (f ` S)" "bounded (g ` S)" shows "bounded ((\x. dist (f x) (g x)) ` S)" proof - from assms obtain M1 M2 where *: "dist (f x) undefined \ M1" "dist undefined (g x) \ M2" if "x \ S" for x by (auto simp: bounded_any_center[of _ undefined] dist_commute) have "dist (f x) (g x) \ M1 + M2" if "x \ S" for x using *[OF that] by metric then show ?thesis by (auto intro!: boundedI) qed lemma bounded_Times: assumes "bounded s" "bounded t" shows "bounded (s \ t)" proof - obtain x y a b where "\z\s. dist x z \ a" "\z\t. dist y z \ b" using assms [unfolded bounded_def] by auto then have "\z\s \ t. dist (x, y) z \ sqrt (a\<^sup>2 + b\<^sup>2)" by (auto simp: dist_Pair_Pair real_sqrt_le_mono add_mono power_mono) then show ?thesis unfolding bounded_any_center [where a="(x, y)"] by auto qed subsection \Compactness\ lemma compact_imp_bounded: assumes "compact U" shows "bounded U" proof - have "compact U" "\x\U. open (ball x 1)" "U \ (\x\U. ball x 1)" using assms by auto then obtain D where D: "D \ U" "finite D" "U \ (\x\D. ball x 1)" by (metis compactE_image) from \finite D\ have "bounded (\x\D. ball x 1)" by (simp add: bounded_UN) then show "bounded U" using \U \ (\x\D. ball x 1)\ by (rule bounded_subset) qed lemma closure_Int_ball_not_empty: assumes "S \ closure T" "x \ S" "r > 0" shows "T \ ball x r \ {}" using assms centre_in_ball closure_iff_nhds_not_empty by blast lemma compact_sup_maxdistance: - fixes s :: "'a::metric_space set" - assumes "compact s" - and "s \ {}" - shows "\x\s. \y\s. \u\s. \v\s. dist u v \ dist x y" + fixes S :: "'a::metric_space set" + assumes "compact S" + and "S \ {}" + shows "\x\S. \y\S. \u\S. \v\S. dist u v \ dist x y" proof - - have "compact (s \ s)" - using \compact s\ by (intro compact_Times) - moreover have "s \ s \ {}" - using \s \ {}\ by auto - moreover have "continuous_on (s \ s) (\x. dist (fst x) (snd x))" + have "compact (S \ S)" + using \compact S\ by (intro compact_Times) + moreover have "S \ S \ {}" + using \S \ {}\ by auto + moreover have "continuous_on (S \ S) (\x. dist (fst x) (snd x))" by (intro continuous_at_imp_continuous_on ballI continuous_intros) ultimately show ?thesis - using continuous_attains_sup[of "s \ s" "\x. dist (fst x) (snd x)"] by auto + using continuous_attains_sup[of "S \ S" "\x. dist (fst x) (snd x)"] by auto qed subsubsection\Totally bounded\ -lemma cauchy_def: "Cauchy s \ (\e>0. \N. \m n. m \ N \ n \ N \ dist (s m) (s n) < e)" +lemma cauchy_def: "Cauchy S \ (\e>0. \N. \m n. m \ N \ n \ N \ dist (S m) (S n) < e)" unfolding Cauchy_def by metis proposition seq_compact_imp_totally_bounded: - assumes "seq_compact s" - shows "\e>0. \k. finite k \ k \ s \ s \ (\x\k. ball x e)" + assumes "seq_compact S" + shows "\e>0. \k. finite k \ k \ S \ S \ (\x\k. ball x e)" proof - - { fix e::real assume "e > 0" assume *: "\k. finite k \ k \ s \ \ s \ (\x\k. ball x e)" - let ?Q = "\x n r. r \ s \ (\m < (n::nat). \ (dist (x m) r < e))" + { fix e::real assume "e > 0" assume *: "\k. finite k \ k \ S \ \ S \ (\x\k. ball x e)" + let ?Q = "\x n r. r \ S \ (\m < (n::nat). \ (dist (x m) r < e))" have "\x. \n::nat. ?Q x n (x n)" proof (rule dependent_wellorder_choice) fix n x assume "\y. y < n \ ?Q x y (x y)" - then have "\ s \ (\x\x ` {0.. S \ (\x\x ` {0..s" "z \ (\x\x ` {0..S" "z \ (\x\x ` {0..r. ?Q x n r" using z by auto qed simp - then obtain x where "\n::nat. x n \ s" and x:"\n m. m < n \ \ (dist (x m) (x n) < e)" + then obtain x where "\n::nat. x n \ S" and x:"\n m. m < n \ \ (dist (x m) (x n) < e)" by blast - then obtain l r where "l \ s" and r:"strict_mono r" and "((x \ r) \ l) sequentially" + then obtain l r where "l \ S" and r:"strict_mono r" and "((x \ r) \ l) sequentially" using assms by (metis seq_compact_def) - from this(3) have "Cauchy (x \ r)" + then have "Cauchy (x \ r)" using LIMSEQ_imp_Cauchy by auto then obtain N::nat where "\m n. N \ m \ N \ n \ dist ((x \ r) m) ((x \ r) n) < e" unfolding cauchy_def using \e > 0\ by blast then have False using x[of "r N" "r (N+1)"] r by (auto simp: strict_mono_def) } then show ?thesis by metis qed subsubsection\Heine-Borel theorem\ proposition seq_compact_imp_Heine_Borel: - fixes s :: "'a :: metric_space set" - assumes "seq_compact s" - shows "compact s" + fixes S :: "'a :: metric_space set" + assumes "seq_compact S" + shows "compact S" proof - - from seq_compact_imp_totally_bounded[OF \seq_compact s\] - obtain f where f: "\e>0. finite (f e) \ f e \ s \ s \ (\x\f e. ball x e)" + from seq_compact_imp_totally_bounded[OF \seq_compact S\] + obtain f where f: "\e>0. finite (f e) \ f e \ S \ S \ (\x\f e. ball x e)" unfolding choice_iff' .. define K where "K = (\(x, r). ball x r) ` ((\e \ \ \ {0 <..}. f e) \ \)" - have "countably_compact s" - using \seq_compact s\ by (rule seq_compact_imp_countably_compact) - then show "compact s" + have "countably_compact S" + using \seq_compact S\ by (rule seq_compact_imp_countably_compact) + then show "compact S" proof (rule countably_compact_imp_compact) show "countable K" unfolding K_def using f by (auto intro: countable_finite countable_subset countable_rat intro!: countable_image countable_SIGMA countable_UN) show "\b\K. open b" by (auto simp: K_def) next fix T x - assume T: "open T" "x \ T" and x: "x \ s" + assume T: "open T" "x \ T" and x: "x \ S" from openE[OF T] obtain e where "0 < e" "ball x e \ T" by auto - then have "0 < e / 2" "ball x (e / 2) \ T" + then have "0 < e/2" "ball x (e/2) \ T" by auto - from Rats_dense_in_real[OF \0 < e / 2\] obtain r where "r \ \" "0 < r" "r < e / 2" + from Rats_dense_in_real[OF \0 < e/2\] obtain r where "r \ \" "0 < r" "r < e/2" by auto - from f[rule_format, of r] \0 < r\ \x \ s\ obtain k where "k \ f r" "x \ ball k r" + from f[rule_format, of r] \0 < r\ \x \ S\ obtain k where "k \ f r" "x \ ball k r" by auto from \r \ \\ \0 < r\ \k \ f r\ have "ball k r \ K" by (auto simp: K_def) - then show "\b\K. x \ b \ b \ s \ T" + then show "\b\K. x \ b \ b \ S \ T" proof (rule bexI[rotated], safe) fix y assume "y \ ball k r" - with \r < e / 2\ \x \ ball k r\ have "dist x y < e" + with \r < e/2\ \x \ ball k r\ have "dist x y < e" by (intro dist_triangle_half_r [of k _ e]) (auto simp: dist_commute) with \ball x e \ T\ show "y \ T" by auto next show "x \ ball k r" by fact qed qed qed proposition compact_eq_seq_compact_metric: - "compact (s :: 'a::metric_space set) \ seq_compact s" + "compact (S :: 'a::metric_space set) \ seq_compact S" using compact_imp_seq_compact seq_compact_imp_Heine_Borel by blast proposition compact_def: \ \this is the definition of compactness in HOL Light\ "compact (S :: 'a::metric_space set) \ (\f. (\n. f n \ S) \ (\l\S. \r::nat\nat. strict_mono r \ (f \ r) \ l))" unfolding compact_eq_seq_compact_metric seq_compact_def by auto subsubsection \Complete the chain of compactness variants\ proposition compact_eq_Bolzano_Weierstrass: - fixes s :: "'a::metric_space set" - shows "compact s \ (\t. infinite t \ t \ s --> (\x \ s. x islimpt t))" - (is "?lhs = ?rhs") -proof - assume ?lhs - then show ?rhs - using Heine_Borel_imp_Bolzano_Weierstrass[of s] by auto -next - assume ?rhs - then show ?lhs - unfolding compact_eq_seq_compact_metric by (rule Bolzano_Weierstrass_imp_seq_compact) -qed + fixes S :: "'a::metric_space set" + shows "compact S \ (\T. infinite T \ T \ S \ (\x \ S. x islimpt T))" + using Bolzano_Weierstrass_imp_seq_compact Heine_Borel_imp_Bolzano_Weierstrass compact_eq_seq_compact_metric + by blast proposition Bolzano_Weierstrass_imp_bounded: - "\t. infinite t \ t \ s \ (\x \ s. x islimpt t) \ bounded s" - using compact_imp_bounded unfolding compact_eq_Bolzano_Weierstrass . + "(\T. \infinite T; T \ S\ \ (\x \ S. x islimpt T)) \ bounded S" + using compact_imp_bounded unfolding compact_eq_Bolzano_Weierstrass by metis subsection \Banach fixed point theorem\ theorem banach_fix:\ \TODO: rename to \Banach_fix\\ assumes s: "complete s" "s \ {}" and c: "0 \ c" "c < 1" and f: "f ` s \ s" and lipschitz: "\x\s. \y\s. dist (f x) (f y) \ c * dist x y" shows "\!x\s. f x = x" proof - from c have "1 - c > 0" by simp from s(2) obtain z0 where z0: "z0 \ s" by blast define z where "z n = (f ^^ n) z0" for n with f z0 have z_in_s: "z n \ s" for n :: nat by (induct n) auto define d where "d = dist (z 0) (z 1)" have fzn: "f (z n) = z (Suc n)" for n by (simp add: z_def) have cf_z: "dist (z n) (z (Suc n)) \ (c ^ n) * d" for n :: nat proof (induct n) case 0 then show ?case by (simp add: d_def) next case (Suc m) with \0 \ c\ have "c * dist (z m) (z (Suc m)) \ c ^ Suc m * d" using mult_left_mono[of "dist (z m) (z (Suc m))" "c ^ m * d" c] by simp then show ?case using lipschitz[THEN bspec[where x="z m"], OF z_in_s, THEN bspec[where x="z (Suc m)"], OF z_in_s] by (simp add: fzn mult_le_cancel_left) qed have cf_z2: "(1 - c) * dist (z m) (z (m + n)) \ (c ^ m) * d * (1 - c ^ n)" for n m :: nat proof (induct n) case 0 show ?case by simp next case (Suc k) from c have "(1 - c) * dist (z m) (z (m + Suc k)) \ (1 - c) * (dist (z m) (z (m + k)) + dist (z (m + k)) (z (Suc (m + k))))" by (simp add: dist_triangle) also from c cf_z[of "m + k"] have "\ \ (1 - c) * (dist (z m) (z (m + k)) + c ^ (m + k) * d)" by simp also from Suc have "\ \ c ^ m * d * (1 - c ^ k) + (1 - c) * c ^ (m + k) * d" by (simp add: field_simps) also have "\ = (c ^ m) * (d * (1 - c ^ k) + (1 - c) * c ^ k * d)" by (simp add: power_add field_simps) also from c have "\ \ (c ^ m) * d * (1 - c ^ Suc k)" by (simp add: field_simps) finally show ?case by simp qed have "\N. \m n. N \ m \ N \ n \ dist (z m) (z n) < e" if "e > 0" for e proof (cases "d = 0") case True from \1 - c > 0\ have "(1 - c) * x \ 0 \ x \ 0" for x by (metis mult_zero_left mult.commute real_mult_le_cancel_iff1) with c cf_z2[of 0] True have "z n = z0" for n by (simp add: z_def) with \e > 0\ show ?thesis by simp next case False with zero_le_dist[of "z 0" "z 1"] have "d > 0" by (metis d_def less_le) with \1 - c > 0\ \e > 0\ have "0 < e * (1 - c) / d" by simp with c obtain N where N: "c ^ N < e * (1 - c) / d" using real_arch_pow_inv[of "e * (1 - c) / d" c] by auto have *: "dist (z m) (z n) < e" if "m > n" and as: "m \ N" "n \ N" for m n :: nat proof - from c \n \ N\ have *: "c ^ n \ c ^ N" using power_decreasing[OF \n\N\, of c] by simp from c \m > n\ have "1 - c ^ (m - n) > 0" using power_strict_mono[of c 1 "m - n"] by simp with \d > 0\ \0 < 1 - c\ have **: "d * (1 - c ^ (m - n)) / (1 - c) > 0" by simp from cf_z2[of n "m - n"] \m > n\ have "dist (z m) (z n) \ c ^ n * d * (1 - c ^ (m - n)) / (1 - c)" by (simp add: pos_le_divide_eq[OF \1 - c > 0\] mult.commute dist_commute) also have "\ \ c ^ N * d * (1 - c ^ (m - n)) / (1 - c)" using mult_right_mono[OF * order_less_imp_le[OF **]] by (simp add: mult.assoc) also have "\ < (e * (1 - c) / d) * d * (1 - c ^ (m - n)) / (1 - c)" using mult_strict_right_mono[OF N **] by (auto simp: mult.assoc) also from c \d > 0\ \1 - c > 0\ have "\ = e * (1 - c ^ (m - n))" by simp also from c \1 - c ^ (m - n) > 0\ \e > 0\ have "\ \ e" using mult_right_le_one_le[of e "1 - c ^ (m - n)"] by auto finally show ?thesis by simp qed have "dist (z n) (z m) < e" if "N \ m" "N \ n" for m n :: nat proof (cases "n = m") case True with \e > 0\ show ?thesis by simp next case False with *[of n m] *[of m n] and that show ?thesis by (auto simp: dist_commute nat_neq_iff) qed then show ?thesis by auto qed then have "Cauchy z" by (simp add: cauchy_def) then obtain x where "x\s" and x:"(z \ x) sequentially" using s(1)[unfolded compact_def complete_def, THEN spec[where x=z]] and z_in_s by auto define e where "e = dist (f x) x" have "e = 0" proof (rule ccontr) assume "e \ 0" then have "e > 0" unfolding e_def using zero_le_dist[of "f x" x] by (metis dist_eq_0_iff dist_nz e_def) - then obtain N where N:"\n\N. dist (z n) x < e / 2" + then obtain N where N:"\n\N. dist (z n) x < e/2" using x[unfolded lim_sequentially, THEN spec[where x="e/2"]] by auto - then have N':"dist (z N) x < e / 2" by auto + then have N':"dist (z N) x < e/2" by auto have *: "c * dist (z N) x \ dist (z N) x" unfolding mult_le_cancel_right2 using zero_le_dist[of "z N" x] and c by (metis dist_eq_0_iff dist_nz order_less_asym less_le) have "dist (f (z N)) (f x) \ c * dist (z N) x" using lipschitz[THEN bspec[where x="z N"], THEN bspec[where x=x]] using z_in_s[of N] \x\s\ using c by auto - also have "\ < e / 2" + also have "\ < e/2" using N' and c using * by auto finally show False unfolding fzn using N[THEN spec[where x="Suc N"]] and dist_triangle_half_r[of "z (Suc N)" "f x" e x] unfolding e_def by auto qed then have "f x = x" by (auto simp: e_def) moreover have "y = x" if "f y = y" "y \ s" for y proof - from \x \ s\ \f x = x\ that have "dist x y \ c * dist x y" using lipschitz[THEN bspec[where x=x], THEN bspec[where x=y]] by simp with c and zero_le_dist[of x y] have "dist x y = 0" by (simp add: mult_le_cancel_right1) then show ?thesis by simp qed ultimately show ?thesis using \x\s\ by blast qed subsection \Edelstein fixed point theorem\ -theorem edelstein_fix:\ \TODO: rename to \Edelstein_fix\\ - fixes s :: "'a::metric_space set" - assumes s: "compact s" "s \ {}" - and gs: "(g ` s) \ s" - and dist: "\x\s. \y\s. x \ y \ dist (g x) (g y) < dist x y" - shows "\!x\s. g x = x" +theorem Edelstein_fix: + fixes S :: "'a::metric_space set" + assumes S: "compact S" "S \ {}" + and gs: "(g ` S) \ S" + and dist: "\x\S. \y\S. x \ y \ dist (g x) (g y) < dist x y" + shows "\!x\S. g x = x" proof - - let ?D = "(\x. (x, x)) ` s" + let ?D = "(\x. (x, x)) ` S" have D: "compact ?D" "?D \ {}" by (rule compact_continuous_image) - (auto intro!: s continuous_Pair continuous_ident simp: continuous_on_eq_continuous_within) - - have "\x y e. x \ s \ y \ s \ 0 < e \ dist y x < e \ dist (g y) (g x) < e" + (auto intro!: S continuous_Pair continuous_ident simp: continuous_on_eq_continuous_within) + + have "\x y e. x \ S \ y \ S \ 0 < e \ dist y x < e \ dist (g y) (g x) < e" using dist by fastforce - then have "continuous_on s g" + then have "continuous_on S g" by (auto simp: continuous_on_iff) then have cont: "continuous_on ?D (\x. dist ((g \ fst) x) (snd x))" unfolding continuous_on_eq_continuous_within by (intro continuous_dist ballI continuous_within_compose) (auto intro!: continuous_fst continuous_snd continuous_ident simp: image_image) - obtain a where "a \ s" and le: "\x. x \ s \ dist (g a) a \ dist (g x) x" + obtain a where "a \ S" and le: "\x. x \ S \ dist (g a) a \ dist (g x) x" using continuous_attains_inf[OF D cont] by auto have "g a = a" proof (rule ccontr) assume "g a \ a" - with \a \ s\ gs have "dist (g (g a)) (g a) < dist (g a) a" + with \a \ S\ gs have "dist (g (g a)) (g a) < dist (g a) a" by (intro dist[rule_format]) auto moreover have "dist (g a) a \ dist (g (g a)) (g a)" - using \a \ s\ gs by (intro le) auto + using \a \ S\ gs by (intro le) auto ultimately show False by auto qed - moreover have "\x. x \ s \ g x = x \ x = a" - using dist[THEN bspec[where x=a]] \g a = a\ and \a\s\ by auto - ultimately show "\!x\s. g x = x" - using \a \ s\ by blast + moreover have "\x. x \ S \ g x = x \ x = a" + using dist[THEN bspec[where x=a]] \g a = a\ and \a\S\ by auto + ultimately show "\!x\S. g x = x" + using \a \ S\ by blast qed subsection \The diameter of a set\ definition\<^marker>\tag important\ diameter :: "'a::metric_space set \ real" where "diameter S = (if S = {} then 0 else SUP (x,y)\S\S. dist x y)" lemma diameter_empty [simp]: "diameter{} = 0" by (auto simp: diameter_def) lemma diameter_singleton [simp]: "diameter{x} = 0" by (auto simp: diameter_def) lemma diameter_le: assumes "S \ {} \ 0 \ d" - and no: "\x y. \x \ S; y \ S\ \ norm(x - y) \ d" - shows "diameter S \ d" -using assms + and no: "\x y. \x \ S; y \ S\ \ norm(x - y) \ d" + shows "diameter S \ d" + using assms by (auto simp: dist_norm diameter_def intro: cSUP_least) lemma diameter_bounded_bound: - fixes s :: "'a :: metric_space set" - assumes s: "bounded s" "x \ s" "y \ s" - shows "dist x y \ diameter s" + fixes S :: "'a :: metric_space set" + assumes S: "bounded S" "x \ S" "y \ S" + shows "dist x y \ diameter S" proof - - from s obtain z d where z: "\x. x \ s \ dist z x \ d" + from S obtain z d where z: "\x. x \ S \ dist z x \ d" unfolding bounded_def by auto - have "bdd_above (case_prod dist ` (s\s))" + have "bdd_above (case_prod dist ` (S\S))" proof (intro bdd_aboveI, safe) fix a b - assume "a \ s" "b \ s" + assume "a \ S" "b \ S" with z[of a] z[of b] dist_triangle[of a b z] show "dist a b \ 2 * d" by (simp add: dist_commute) qed - moreover have "(x,y) \ s\s" using s by auto - ultimately have "dist x y \ (SUP (x,y)\s\s. dist x y)" + moreover have "(x,y) \ S\S" using S by auto + ultimately have "dist x y \ (SUP (x,y)\S\S. dist x y)" by (rule cSUP_upper2) simp - with \x \ s\ show ?thesis + with \x \ S\ show ?thesis by (auto simp: diameter_def) qed lemma diameter_lower_bounded: - fixes s :: "'a :: metric_space set" - assumes s: "bounded s" - and d: "0 < d" "d < diameter s" - shows "\x\s. \y\s. d < dist x y" + fixes S :: "'a :: metric_space set" + assumes S: "bounded S" + and d: "0 < d" "d < diameter S" + shows "\x\S. \y\S. d < dist x y" proof (rule ccontr) assume contr: "\ ?thesis" - moreover have "s \ {}" + moreover have "S \ {}" using d by (auto simp: diameter_def) - ultimately have "diameter s \ d" + ultimately have "diameter S \ d" by (auto simp: not_less diameter_def intro!: cSUP_least) - with \d < diameter s\ show False by auto + with \d < diameter S\ show False by auto qed lemma diameter_bounded: - assumes "bounded s" - shows "\x\s. \y\s. dist x y \ diameter s" - and "\d>0. d < diameter s \ (\x\s. \y\s. dist x y > d)" - using diameter_bounded_bound[of s] diameter_lower_bounded[of s] assms + assumes "bounded S" + shows "\x\S. \y\S. dist x y \ diameter S" + and "\d>0. d < diameter S \ (\x\S. \y\S. dist x y > d)" + using diameter_bounded_bound[of S] diameter_lower_bounded[of S] assms by auto -lemma bounded_two_points: - "bounded S \ (\e. \x\S. \y\S. dist x y \ e)" - apply (rule iffI) - subgoal using diameter_bounded(1) by auto - subgoal using bounded_any_center[of S] by meson - done +lemma bounded_two_points: "bounded S \ (\e. \x\S. \y\S. dist x y \ e)" + by (meson bounded_def diameter_bounded(1)) lemma diameter_compact_attained: - assumes "compact s" - and "s \ {}" - shows "\x\s. \y\s. dist x y = diameter s" + assumes "compact S" + and "S \ {}" + shows "\x\S. \y\S. dist x y = diameter S" proof - - have b: "bounded s" using assms(1) + have b: "bounded S" using assms(1) by (rule compact_imp_bounded) - then obtain x y where xys: "x\s" "y\s" - and xy: "\u\s. \v\s. dist u v \ dist x y" + then obtain x y where xys: "x\S" "y\S" + and xy: "\u\S. \v\S. dist u v \ dist x y" using compact_sup_maxdistance[OF assms] by auto - then have "diameter s \ dist x y" + then have "diameter S \ dist x y" unfolding diameter_def apply clarsimp apply (rule cSUP_least, fast+) done then show ?thesis by (metis b diameter_bounded_bound order_antisym xys) qed lemma diameter_ge_0: assumes "bounded S" shows "0 \ diameter S" by (metis all_not_in_conv assms diameter_bounded_bound diameter_empty dist_self order_refl) lemma diameter_subset: assumes "S \ T" "bounded T" shows "diameter S \ diameter T" proof (cases "S = {} \ T = {}") case True with assms show ?thesis by (force simp: diameter_ge_0) next case False then have "bdd_above ((\x. case x of (x, xa) \ dist x xa) ` (T \ T))" using \bounded T\ diameter_bounded_bound by (force simp: bdd_above_def) with False \S \ T\ show ?thesis apply (simp add: diameter_def) apply (rule cSUP_subset_mono, auto) done qed lemma diameter_closure: assumes "bounded S" shows "diameter(closure S) = diameter S" proof (rule order_antisym) have "False" if "diameter S < diameter (closure S)" proof - define d where "d = diameter(closure S) - diameter(S)" have "d > 0" using that by (simp add: d_def) then have "diameter(closure(S)) - d / 2 < diameter(closure(S))" by simp have dd: "diameter (closure S) - d / 2 = (diameter(closure(S)) + diameter(S)) / 2" by (simp add: d_def field_split_simps) have bocl: "bounded (closure S)" using assms by blast moreover have "0 \ diameter S" using assms diameter_ge_0 by blast ultimately obtain x y where "x \ closure S" "y \ closure S" and xy: "diameter(closure(S)) - d / 2 < dist x y" using diameter_bounded(2) [OF bocl, rule_format, of "diameter(closure(S)) - d / 2"] \d > 0\ d_def by auto then obtain x' y' where x'y': "x' \ S" "dist x' x < d/4" "y' \ S" "dist y' y < d/4" using closure_approachable by (metis \0 < d\ zero_less_divide_iff zero_less_numeral) then have "dist x' y' \ diameter S" using assms diameter_bounded_bound by blast with x'y' have "dist x y \ d / 4 + diameter S + d / 4" by (meson add_mono_thms_linordered_semiring(1) dist_triangle dist_triangle3 less_eq_real_def order_trans) then show ?thesis using xy d_def by linarith qed then show "diameter (closure S) \ diameter S" by fastforce next show "diameter S \ diameter (closure S)" by (simp add: assms bounded_closure closure_subset diameter_subset) qed proposition Lebesgue_number_lemma: assumes "compact S" "\ \ {}" "S \ \\" and ope: "\B. B \ \ \ open B" obtains \ where "0 < \" "\T. \T \ S; diameter T < \\ \ \B \ \. T \ B" proof (cases "S = {}") case True then show ?thesis by (metis \\ \ {}\ zero_less_one empty_subsetI equals0I subset_trans that) next case False { fix x assume "x \ S" then obtain C where C: "x \ C" "C \ \" using \S \ \\\ by blast then obtain r where r: "r>0" "ball x (2*r) \ C" by (metis mult.commute mult_2_right not_le ope openE field_sum_of_halves zero_le_numeral zero_less_mult_iff) then have "\r C. r > 0 \ ball x (2*r) \ C \ C \ \" using C by blast } then obtain r where r: "\x. x \ S \ r x > 0 \ (\C \ \. ball x (2*r x) \ C)" by metis then have "S \ (\x \ S. ball x (r x))" by auto then obtain \ where "finite \" "S \ \\" and \: "\ \ (\x. ball x (r x)) ` S" by (rule compactE [OF \compact S\]) auto then obtain S0 where "S0 \ S" "finite S0" and S0: "\ = (\x. ball x (r x)) ` S0" by (meson finite_subset_image) then have "S0 \ {}" using False \S \ \\\ by auto define \ where "\ = Inf (r ` S0)" have "\ > 0" using \finite S0\ \S0 \ S\ \S0 \ {}\ r by (auto simp: \_def finite_less_Inf_iff) show ?thesis proof show "0 < \" by (simp add: \0 < \\) show "\B \ \. T \ B" if "T \ S" and dia: "diameter T < \" for T proof (cases "T = {}") case True then show ?thesis using \\ \ {}\ by blast next case False then obtain y where "y \ T" by blast then have "y \ S" using \T \ S\ by auto then obtain x where "x \ S0" and x: "y \ ball x (r x)" using \S \ \\\ S0 that by blast have "ball y \ \ ball y (r x)" by (metis \_def \S0 \ {}\ \finite S0\ \x \ S0\ empty_is_image finite_imageI finite_less_Inf_iff imageI less_irrefl not_le subset_ball) also have "... \ ball x (2*r x)" using x by metric finally obtain C where "C \ \" "ball y \ \ C" by (meson r \S0 \ S\ \x \ S0\ dual_order.trans subsetCE) have "bounded T" using \compact S\ bounded_subset compact_imp_bounded \T \ S\ by blast then have "T \ ball y \" using \y \ T\ dia diameter_bounded_bound by fastforce then show ?thesis apply (rule_tac x=C in bexI) using \ball y \ \ C\ \C \ \\ by auto qed qed qed subsection \Metric spaces with the Heine-Borel property\ text \ A metric space (or topological vector space) is said to have the Heine-Borel property if every closed and bounded subset is compact. \ class heine_borel = metric_space + assumes bounded_imp_convergent_subsequence: "bounded (range f) \ \l r. strict_mono (r::nat\nat) \ ((f \ r) \ l) sequentially" proposition bounded_closed_imp_seq_compact: - fixes s::"'a::heine_borel set" - assumes "bounded s" - and "closed s" - shows "seq_compact s" + fixes S::"'a::heine_borel set" + assumes "bounded S" + and "closed S" + shows "seq_compact S" proof (unfold seq_compact_def, clarify) fix f :: "nat \ 'a" - assume f: "\n. f n \ s" - with \bounded s\ have "bounded (range f)" + assume f: "\n. f n \ S" + with \bounded S\ have "bounded (range f)" by (auto intro: bounded_subset) obtain l r where r: "strict_mono (r :: nat \ nat)" and l: "((f \ r) \ l) sequentially" using bounded_imp_convergent_subsequence [OF \bounded (range f)\] by auto - from f have fr: "\n. (f \ r) n \ s" + from f have fr: "\n. (f \ r) n \ S" by simp - have "l \ s" using \closed s\ fr l + have "l \ S" using \closed S\ fr l by (rule closed_sequentially) - show "\l\s. \r. strict_mono r \ ((f \ r) \ l) sequentially" - using \l \ s\ r l by blast + show "\l\S. \r. strict_mono r \ ((f \ r) \ l) sequentially" + using \l \ S\ r l by blast qed lemma compact_eq_bounded_closed: - fixes s :: "'a::heine_borel set" - shows "compact s \ bounded s \ closed s" - (is "?lhs = ?rhs") -proof - assume ?lhs - then show ?rhs - using compact_imp_closed compact_imp_bounded - by blast -next - assume ?rhs - then show ?lhs - using bounded_closed_imp_seq_compact[of s] - unfolding compact_eq_seq_compact_metric - by auto -qed + fixes S :: "'a::heine_borel set" + shows "compact S \ bounded S \ closed S" + using bounded_closed_imp_seq_compact compact_eq_seq_compact_metric compact_imp_bounded compact_imp_closed + by auto lemma compact_Inter: fixes \ :: "'a :: heine_borel set set" assumes com: "\S. S \ \ \ compact S" and "\ \ {}" shows "compact(\ \)" using assms by (meson Inf_lower all_not_in_conv bounded_subset closed_Inter compact_eq_bounded_closed) lemma compact_closure [simp]: fixes S :: "'a::heine_borel set" shows "compact(closure S) \ bounded S" by (meson bounded_closure bounded_subset closed_closure closure_subset compact_eq_bounded_closed) instance\<^marker>\tag important\ real :: heine_borel proof fix f :: "nat \ real" assume f: "bounded (range f)" obtain r :: "nat \ nat" where r: "strict_mono r" "monoseq (f \ r)" unfolding comp_def by (metis seq_monosub) then have "Bseq (f \ r)" unfolding Bseq_eq_bounded using f by (metis BseqI' bounded_iff comp_apply rangeI) with r show "\l r. strict_mono r \ (f \ r) \ l" using Bseq_monoseq_convergent[of "f \ r"] by (auto simp: convergent_def) qed lemma compact_lemma_general: fixes f :: "nat \ 'a" fixes proj::"'a \ 'b \ 'c::heine_borel" (infixl "proj" 60) fixes unproj:: "('b \ 'c) \ 'a" assumes finite_basis: "finite basis" assumes bounded_proj: "\k. k \ basis \ bounded ((\x. x proj k) ` range f)" assumes proj_unproj: "\e k. k \ basis \ (unproj e) proj k = e k" assumes unproj_proj: "\x. unproj (\k. x proj k) = x" shows "\d\basis. \l::'a. \ r::nat\nat. strict_mono r \ (\e>0. eventually (\n. \i\d. dist (f (r n) proj i) (l proj i) < e) sequentially)" proof safe fix d :: "'b set" assume d: "d \ basis" with finite_basis have "finite d" by (blast intro: finite_subset) from this d show "\l::'a. \r::nat\nat. strict_mono r \ (\e>0. eventually (\n. \i\d. dist (f (r n) proj i) (l proj i) < e) sequentially)" proof (induct d) case empty then show ?case unfolding strict_mono_def by auto next case (insert k d) have k[intro]: "k \ basis" using insert by auto have s': "bounded ((\x. x proj k) ` range f)" using k by (rule bounded_proj) obtain l1::"'a" and r1 where r1: "strict_mono r1" and lr1: "\e > 0. eventually (\n. \i\d. dist (f (r1 n) proj i) (l1 proj i) < e) sequentially" using insert(3) using insert(4) by auto have f': "\n. f (r1 n) proj k \ (\x. x proj k) ` range f" by simp have "bounded (range (\i. f (r1 i) proj k))" by (metis (lifting) bounded_subset f' image_subsetI s') then obtain l2 r2 where r2:"strict_mono r2" and lr2:"((\i. f (r1 (r2 i)) proj k) \ l2) sequentially" using bounded_imp_convergent_subsequence[of "\i. f (r1 i) proj k"] by (auto simp: o_def) define r where "r = r1 \ r2" have r:"strict_mono r" using r1 and r2 unfolding r_def o_def strict_mono_def by auto moreover define l where "l = unproj (\i. if i = k then l2 else l1 proj i)" { fix e::real assume "e > 0" from lr1 \e > 0\ have N1: "eventually (\n. \i\d. dist (f (r1 n) proj i) (l1 proj i) < e) sequentially" by blast from lr2 \e > 0\ have N2:"eventually (\n. dist (f (r1 (r2 n)) proj k) l2 < e) sequentially" by (rule tendstoD) from r2 N1 have N1': "eventually (\n. \i\d. dist (f (r1 (r2 n)) proj i) (l1 proj i) < e) sequentially" by (rule eventually_subseq) have "eventually (\n. \i\(insert k d). dist (f (r n) proj i) (l proj i) < e) sequentially" using N1' N2 by eventually_elim (insert insert.prems, auto simp: l_def r_def o_def proj_unproj) } ultimately show ?case by auto qed qed lemma bounded_fst: "bounded s \ bounded (fst ` s)" unfolding bounded_def by (metis (erased, hide_lams) dist_fst_le image_iff order_trans) lemma bounded_snd: "bounded s \ bounded (snd ` s)" unfolding bounded_def by (metis (no_types, hide_lams) dist_snd_le image_iff order.trans) instance\<^marker>\tag important\ prod :: (heine_borel, heine_borel) heine_borel proof fix f :: "nat \ 'a \ 'b" assume f: "bounded (range f)" then have "bounded (fst ` range f)" by (rule bounded_fst) then have s1: "bounded (range (fst \ f))" by (simp add: image_comp) obtain l1 r1 where r1: "strict_mono r1" and l1: "(\n. fst (f (r1 n))) \ l1" using bounded_imp_convergent_subsequence [OF s1] unfolding o_def by fast from f have s2: "bounded (range (snd \ f \ r1))" by (auto simp: image_comp intro: bounded_snd bounded_subset) obtain l2 r2 where r2: "strict_mono r2" and l2: "((\n. snd (f (r1 (r2 n)))) \ l2) sequentially" using bounded_imp_convergent_subsequence [OF s2] unfolding o_def by fast have l1': "((\n. fst (f (r1 (r2 n)))) \ l1) sequentially" using LIMSEQ_subseq_LIMSEQ [OF l1 r2] unfolding o_def . have l: "((f \ (r1 \ r2)) \ (l1, l2)) sequentially" using tendsto_Pair [OF l1' l2] unfolding o_def by simp have r: "strict_mono (r1 \ r2)" using r1 r2 unfolding strict_mono_def by simp show "\l r. strict_mono r \ ((f \ r) \ l) sequentially" using l r by fast qed subsection \Completeness\ proposition (in metric_space) completeI: assumes "\f. \n. f n \ s \ Cauchy f \ \l\s. f \ l" shows "complete s" using assms unfolding complete_def by fast proposition (in metric_space) completeE: assumes "complete s" and "\n. f n \ s" and "Cauchy f" obtains l where "l \ s" and "f \ l" using assms unfolding complete_def by fast (* TODO: generalize to uniform spaces *) lemma compact_imp_complete: fixes s :: "'a::metric_space set" assumes "compact s" shows "complete s" proof - { fix f assume as: "(\n::nat. f n \ s)" "Cauchy f" from as(1) obtain l r where lr: "l\s" "strict_mono r" "(f \ r) \ l" using assms unfolding compact_def by blast note lr' = seq_suble [OF lr(2)] { fix e :: real assume "e > 0" from as(2) obtain N where N:"\m n. N \ m \ N \ n \ dist (f m) (f n) < e/2" unfolding cauchy_def using \e > 0\ apply (erule_tac x="e/2" in allE, auto) done from lr(3)[unfolded lim_sequentially, THEN spec[where x="e/2"]] obtain M where M:"\n\M. dist ((f \ r) n) l < e/2" using \e > 0\ by auto { fix n :: nat assume n: "n \ max N M" have "dist ((f \ r) n) l < e/2" using n M by auto moreover have "r n \ N" using lr'[of n] n by auto - then have "dist (f n) ((f \ r) n) < e / 2" + then have "dist (f n) ((f \ r) n) < e/2" using N and n by auto ultimately have "dist (f n) l < e" using n M by metric } then have "\N. \n\N. dist (f n) l < e" by blast } then have "\l\s. (f \ l) sequentially" using \l\s\ unfolding lim_sequentially by auto } then show ?thesis unfolding complete_def by auto qed proposition compact_eq_totally_bounded: "compact s \ complete s \ (\e>0. \k. finite k \ s \ (\x\k. ball x e))" (is "_ \ ?rhs") proof assume assms: "?rhs" then obtain k where k: "\e. 0 < e \ finite (k e)" "\e. 0 < e \ s \ (\x\k e. ball x e)" by (auto simp: choice_iff') show "compact s" proof cases assume "s = {}" then show "compact s" by (simp add: compact_def) next assume "s \ {}" show ?thesis unfolding compact_def proof safe fix f :: "nat \ 'a" assume f: "\n. f n \ s" define e where "e n = 1 / (2 * Suc n)" for n then have [simp]: "\n. 0 < e n" by auto define B where "B n U = (SOME b. infinite {n. f n \ b} \ (\x. b \ ball x (e n) \ U))" for n U { fix n U assume "infinite {n. f n \ U}" then have "\b\k (e n). infinite {i\{n. f n \ U}. f i \ ball b (e n)}" using k f by (intro pigeonhole_infinite_rel) (auto simp: subset_eq) then obtain a where "a \ k (e n)" "infinite {i \ {n. f n \ U}. f i \ ball a (e n)}" .. then have "\b. infinite {i. f i \ b} \ (\x. b \ ball x (e n) \ U)" by (intro exI[of _ "ball a (e n) \ U"] exI[of _ a]) (auto simp: ac_simps) from someI_ex[OF this] have "infinite {i. f i \ B n U}" "\x. B n U \ ball x (e n) \ U" unfolding B_def by auto } note B = this define F where "F = rec_nat (B 0 UNIV) B" { fix n have "infinite {i. f i \ F n}" by (induct n) (auto simp: F_def B) } then have F: "\n. \x. F (Suc n) \ ball x (e n) \ F n" using B by (simp add: F_def) then have F_dec: "\m n. m \ n \ F n \ F m" using decseq_SucI[of F] by (auto simp: decseq_def) obtain sel where sel: "\k i. i < sel k i" "\k i. f (sel k i) \ F k" proof (atomize_elim, unfold all_conj_distrib[symmetric], intro choice allI) fix k i have "infinite ({n. f n \ F k} - {.. i})" using \infinite {n. f n \ F k}\ by auto from infinite_imp_nonempty[OF this] show "\x>i. f x \ F k" by (simp add: set_eq_iff not_le conj_commute) qed define t where "t = rec_nat (sel 0 0) (\n i. sel (Suc n) i)" have "strict_mono t" unfolding strict_mono_Suc_iff by (simp add: t_def sel) moreover have "\i. (f \ t) i \ s" using f by auto moreover - { - fix n - have "(f \ t) n \ F n" - by (cases n) (simp_all add: t_def sel) - } - note t = this + have t: "(f \ t) n \ F n" for n + by (cases n) (simp_all add: t_def sel) have "Cauchy (f \ t)" proof (safe intro!: metric_CauchyI exI elim!: nat_approx_posE) fix r :: real and N n m assume "1 / Suc N < r" "Suc N \ n" "Suc N \ m" then have "(f \ t) n \ F (Suc N)" "(f \ t) m \ F (Suc N)" "2 * e N < r" using F_dec t by (auto simp: e_def field_simps) with F[of N] obtain x where "dist x ((f \ t) n) < e N" "dist x ((f \ t) m) < e N" by (auto simp: subset_eq) with \2 * e N < r\ show "dist ((f \ t) m) ((f \ t) n) < r" by metric qed ultimately show "\l\s. \r. strict_mono r \ (f \ r) \ l" using assms unfolding complete_def by blast qed qed qed (metis compact_imp_complete compact_imp_seq_compact seq_compact_imp_totally_bounded) lemma cauchy_imp_bounded: assumes "Cauchy s" shows "bounded (range s)" proof - from assms obtain N :: nat where "\m n. N \ m \ N \ n \ dist (s m) (s n) < 1" unfolding cauchy_def by force then have N:"\n. N \ n \ dist (s N) (s n) < 1" by auto moreover have "bounded (s ` {0..N})" using finite_imp_bounded[of "s ` {1..N}"] by auto then obtain a where a:"\x\s ` {0..N}. dist (s N) x \ a" unfolding bounded_any_center [where a="s N"] by auto ultimately show "?thesis" unfolding bounded_any_center [where a="s N"] apply (rule_tac x="max a 1" in exI, auto) apply (erule_tac x=y in allE) apply (erule_tac x=y in ballE, auto) done qed instance heine_borel < complete_space proof fix f :: "nat \ 'a" assume "Cauchy f" then have "bounded (range f)" by (rule cauchy_imp_bounded) then have "compact (closure (range f))" unfolding compact_eq_bounded_closed by auto then have "complete (closure (range f))" by (rule compact_imp_complete) moreover have "\n. f n \ closure (range f)" using closure_subset [of "range f"] by auto ultimately have "\l\closure (range f). (f \ l) sequentially" using \Cauchy f\ unfolding complete_def by auto then show "convergent f" unfolding convergent_def by auto qed lemma complete_UNIV: "complete (UNIV :: ('a::complete_space) set)" proof (rule completeI) fix f :: "nat \ 'a" assume "Cauchy f" then have "convergent f" by (rule Cauchy_convergent) then show "\l\UNIV. f \ l" unfolding convergent_def by simp qed lemma complete_imp_closed: fixes S :: "'a::metric_space set" assumes "complete S" shows "closed S" proof (unfold closed_sequential_limits, clarify) fix f x assume "\n. f n \ S" and "f \ x" from \f \ x\ have "Cauchy f" by (rule LIMSEQ_imp_Cauchy) with \complete S\ and \\n. f n \ S\ obtain l where "l \ S" and "f \ l" by (rule completeE) from \f \ x\ and \f \ l\ have "x = l" by (rule LIMSEQ_unique) with \l \ S\ show "x \ S" by simp qed lemma complete_Int_closed: fixes S :: "'a::metric_space set" assumes "complete S" and "closed t" shows "complete (S \ t)" proof (rule completeI) fix f assume "\n. f n \ S \ t" and "Cauchy f" then have "\n. f n \ S" and "\n. f n \ t" by simp_all from \complete S\ obtain l where "l \ S" and "f \ l" using \\n. f n \ S\ and \Cauchy f\ by (rule completeE) from \closed t\ and \\n. f n \ t\ and \f \ l\ have "l \ t" by (rule closed_sequentially) with \l \ S\ and \f \ l\ show "\l\S \ t. f \ l" by fast qed lemma complete_closed_subset: fixes S :: "'a::metric_space set" assumes "closed S" and "S \ t" and "complete t" shows "complete S" using assms complete_Int_closed [of t S] by (simp add: Int_absorb1) lemma complete_eq_closed: fixes S :: "('a::complete_space) set" shows "complete S \ closed S" proof assume "closed S" then show "complete S" using subset_UNIV complete_UNIV by (rule complete_closed_subset) next assume "complete S" then show "closed S" by (rule complete_imp_closed) qed lemma convergent_eq_Cauchy: fixes S :: "nat \ 'a::complete_space" shows "(\l. (S \ l) sequentially) \ Cauchy S" unfolding Cauchy_convergent_iff convergent_def .. lemma convergent_imp_bounded: fixes S :: "nat \ 'a::metric_space" shows "(S \ l) sequentially \ bounded (range S)" by (intro cauchy_imp_bounded LIMSEQ_imp_Cauchy) lemma frontier_subset_compact: fixes S :: "'a::heine_borel set" shows "compact S \ frontier S \ S" using frontier_subset_closed compact_eq_bounded_closed by blast lemma continuous_closed_imp_Cauchy_continuous: fixes S :: "('a::complete_space) set" shows "\continuous_on S f; closed S; Cauchy \; \n. (\ n) \ S\ \ Cauchy(f \ \)" apply (simp add: complete_eq_closed [symmetric] continuous_on_sequentially) by (meson LIMSEQ_imp_Cauchy complete_def) lemma banach_fix_type: fixes f::"'a::complete_space\'a" assumes c:"0 \ c" "c < 1" and lipschitz:"\x. \y. dist (f x) (f y) \ c * dist x y" shows "\!x. (f x = x)" using assms banach_fix[OF complete_UNIV UNIV_not_empty assms(1,2) subset_UNIV, of f] by auto subsection\<^marker>\tag unimportant\\ Finite intersection property\ text\Also developed in HOL's toplogical spaces theory, but the Heine-Borel type class isn't available there.\ lemma closed_imp_fip: fixes S :: "'a::heine_borel set" assumes "closed S" and T: "T \ \" "bounded T" and clof: "\T. T \ \ \ closed T" and none: "\\'. \finite \'; \' \ \\ \ S \ \\' \ {}" shows "S \ \\ \ {}" proof - have "compact (S \ T)" using \closed S\ clof compact_eq_bounded_closed T by blast then have "(S \ T) \ \\ \ {}" apply (rule compact_imp_fip) apply (simp add: clof) by (metis Int_assoc complete_lattice_class.Inf_insert finite_insert insert_subset none \T \ \\) then show ?thesis by blast qed lemma closed_imp_fip_compact: fixes S :: "'a::heine_borel set" shows "\closed S; \T. T \ \ \ compact T; \\'. \finite \'; \' \ \\ \ S \ \\' \ {}\ \ S \ \\ \ {}" by (metis Inf_greatest closed_imp_fip compact_eq_bounded_closed empty_subsetI finite.emptyI inf.orderE) lemma closed_fip_Heine_Borel: fixes \ :: "'a::heine_borel set set" assumes "closed S" "T \ \" "bounded T" and "\T. T \ \ \ closed T" and "\\'. \finite \'; \' \ \\ \ \\' \ {}" shows "\\ \ {}" proof - have "UNIV \ \\ \ {}" using assms closed_imp_fip [OF closed_UNIV] by auto then show ?thesis by simp qed lemma compact_fip_Heine_Borel: fixes \ :: "'a::heine_borel set set" assumes clof: "\T. T \ \ \ compact T" and none: "\\'. \finite \'; \' \ \\ \ \\' \ {}" shows "\\ \ {}" by (metis InterI all_not_in_conv clof closed_fip_Heine_Borel compact_eq_bounded_closed none) lemma compact_sequence_with_limit: fixes f :: "nat \ 'a::heine_borel" shows "(f \ l) sequentially \ compact (insert l (range f))" apply (simp add: compact_eq_bounded_closed, auto) apply (simp add: convergent_imp_bounded) by (simp add: closed_limpt islimpt_insert sequence_unique_limpt) subsection \Properties of Balls and Spheres\ 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 \ 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 \ compact (frontier S)" using compact_eq_bounded_closed compact_frontier_bounded by blast subsection \Distance from a Set\ lemma distance_attains_sup: assumes "compact s" "s \ {}" shows "\x\s. \y\s. dist a y \ dist a x" proof (rule continuous_attains_sup [OF assms]) { fix x assume "x\s" have "(dist a \ 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 \For \emph{minimal} distance, we only need closure, not compactness.\ lemma distance_attains_inf: fixes a :: "'a::heine_borel" assumes "closed s" and "s \ {}" obtains x where "x\s" "\y. y \ s \ dist a x \ dist a y" proof - from assms obtain b where "b \ s" by auto let ?B = "s \ cball a (dist b a)" have "?B \ {}" using \b \ s\ 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 \closed s\ compact_cball) ultimately obtain x where "x \ ?B" "\y\?B. dist a x \ dist a y" by (metis continuous_attains_inf) with that show ?thesis by fastforce qed subsection \Infimum Distance\ definition\<^marker>\tag important\ "infdist x A = (if A = {} then 0 else INF a\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 \ {} \ infdist x A = (INF a\A. dist x a)" by (simp add: infdist_def) lemma infdist_nonneg: "0 \ infdist x A" by (auto simp: infdist_def intro: cINF_greatest) lemma infdist_le: "a \ A \ infdist x A \ dist x a" by (auto intro: cINF_lower simp add: infdist_def) lemma infdist_le2: "a \ A \ dist x a \ d \ infdist x A \ d" by (auto intro!: cINF_lower2 simp add: infdist_def) lemma infdist_zero[simp]: "a \ A \ infdist a A = 0" by (auto intro!: antisym infdist_nonneg infdist_le2) lemma infdist_Un_min: assumes "A \ {}" "B \ {}" shows "infdist x (A \ B) = min (infdist x A) (infdist x B)" using assms by (simp add: infdist_def cINF_union inf_real_def) lemma infdist_triangle: "infdist x A \ 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 \ A" by auto have "infdist x A \ Inf {dist x y + dist y a |a. a \ A}" proof (rule cInf_greatest) from \A \ {}\ show "{dist x y + dist y a |a. a \ A} \ {}" by simp fix d assume "d \ {dist x y + dist y a |a. a \ A}" then obtain a where d: "d = dist x y + dist y a" "a \ A" by auto show "infdist x A \ d" unfolding infdist_notempty[OF \A \ {}\] proof (rule cINF_lower2) show "a \ A" by fact show "dist x a \ d" unfolding d by (rule dist_triangle) qed simp qed also have "\ = dist x y + infdist y A" proof (rule cInf_eq, safe) fix a assume "a \ A" then show "dist x y + infdist y A \ dist x y + dist y a" by (auto intro: infdist_le) next fix i assume inf: "\d. d \ {dist x y + dist y a |a. a \ A} \ i \ d" then have "i - dist x y \ infdist y A" unfolding infdist_notempty[OF \A \ {}\] using \a \ A\ by (intro cINF_greatest) (auto simp: field_simps) then show "i \ dist x y + infdist y A" by simp qed finally show ?thesis by simp qed lemma infdist_triangle_abs: "\infdist x A - infdist y A\ \ dist x y" by (metis (full_types) abs_diff_le_iff diff_le_eq dist_commute infdist_triangle) lemma in_closure_iff_infdist_zero: assumes "A \ {}" shows "x \ closure A \ infdist x A = 0" proof assume "x \ closure A" show "infdist x A = 0" proof (rule ccontr) assume "infdist x A \ 0" with infdist_nonneg[of x A] have "infdist x A > 0" by auto then have "ball x (infdist x A) \ closure A = {}" apply auto apply (metis \x \ closure A\ closure_approachable dist_commute infdist_le not_less) done then have "x \ closure A" by (metis \0 < infdist x A\ centre_in_ball disjoint_iff_not_equal) then show False using \x \ closure A\ by simp qed next assume x: "infdist x A = 0" then obtain a where "a \ A" by atomize_elim (metis all_not_in_conv assms) show "x \ closure A" unfolding closure_approachable apply safe proof (rule ccontr) fix e :: real assume "e > 0" assume "\ (\y\A. dist y x < e)" then have "infdist x A \ e" using \a \ A\ unfolding infdist_def by (force simp: dist_commute intro: cINF_greatest) with x \e > 0\ show False by auto qed qed lemma in_closed_iff_infdist_zero: assumes "closed A" "A \ {}" shows "x \ A \ infdist x A = 0" proof - have "x \ closure A \ 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 \ {}" "x \ 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 \ {}" obtains x where "x \ 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 \ X" "\z. z \ X \ dist y x \ dist y z" by auto have "infdist y X = dist y x" by (auto simp: infdist_def assms intro!: antisym cINF_lower[OF _ \x \ X\] cINF_greatest[OF assms(2) INF(2)]) with \x \ X\ show ?thesis .. qed text \Every metric space is a T4 space:\ instance metric_space \ t4_space proof fix S T::"'a set" assume H: "closed S" "closed T" "S \ T = {}" consider "S = {}" | "T = {}" | "S \ {} \ T \ {}" by auto then show "\U V. open U \ open V \ S \ U \ T \ V \ U \ 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 = (\x\S. ball x ((infdist x T)/2))" have A: "open U" unfolding U_def by auto have "infdist x T > 0" if "x \ S" for x using H that 3 by (auto intro!: infdist_pos_not_in_closed) then have B: "S \ U" unfolding U_def by auto define V where "V = (\x\T. ball x ((infdist x S)/2))" have C: "open V" unfolding V_def by auto have "infdist x S > 0" if "x \ T" for x using H that 3 by (auto intro!: infdist_pos_not_in_closed) then have D: "T \ V" unfolding V_def by auto have "(ball x ((infdist x T)/2)) \ (ball y ((infdist y S)/2)) = {}" if "x \ S" "y \ 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 \ 2 * dist x z + 2 * dist y z" by metric also have "... < infdist x T + infdist y S" using H by auto finally have "dist x y < infdist x T \ dist x y < infdist y S" by auto then show False using infdist_le[OF \x \ S\, of y] infdist_le[OF \y \ T\, of x] by (auto simp add: dist_commute) qed then have E: "U \ 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 \ l) F" shows "((\x. infdist (f x) A) \ infdist l A) F" proof (rule tendstoI) fix e ::real assume "e > 0" from tendstoD[OF f this] show "eventually (\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) \ 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 (\x. infdist (f x) A)" using assms unfolding continuous_def by (rule tendsto_infdist) lemma continuous_on_infdist [continuous_intros]: assumes "continuous_on S f" shows "continuous_on S (\x. infdist (f x) A)" using assms unfolding continuous_on by (auto intro: tendsto_infdist) lemma compact_infdist_le: fixes A::"'a::heine_borel set" assumes "A \ {}" assumes "compact A" assumes "e > 0" shows "compact {x. infdist x A \ e}" proof - from continuous_closed_vimage[of "{0..e}" "\x. infdist x A"] continuous_infdist[OF continuous_ident, of _ UNIV A] have "closed {x. infdist x A \ e}" by (auto simp: vimage_def infdist_nonneg) moreover from assms obtain x0 b where b: "\x. x \ A \ dist x0 x \ b" "closed A" by (auto simp: compact_eq_bounded_closed bounded_def) { fix y assume "infdist y A \ e" moreover from infdist_attains_inf[OF \closed A\ \A \ {}\, of y] obtain z where "z \ A" "infdist y A = dist y z" by blast ultimately have "dist x0 y \ b + e" using b by metric } then have "bounded {x. infdist x A \ e}" by (auto simp: bounded_any_center[where a=x0] intro!: exI[where x="b + e"]) ultimately show "compact {x. infdist x A \ e}" by (simp add: compact_eq_bounded_closed) qed subsection \Separation between Points and Sets\ proposition separate_point_closed: fixes s :: "'a::heine_borel set" assumes "closed s" and "a \ s" shows "\d>0. \x\s. d \ dist a x" proof (cases "s = {}") case True then show ?thesis by(auto intro!: exI[where x=1]) next case False from assms obtain x where "x\s" "\y\s. dist a x \ dist a y" using \s \ {}\ by (blast intro: distance_attains_inf [of s a]) with \x\s\ show ?thesis using dist_pos_lt[of a x] and\a \ s\ by blast qed proposition separate_compact_closed: fixes s t :: "'a::heine_borel set" assumes "compact s" and t: "closed t" "s \ t = {}" shows "\d>0. \x\s. \y\t. d \ dist x y" proof cases assume "s \ {} \ t \ {}" then have "s \ {}" "t \ {}" by auto let ?inf = "\x. infdist x t" have "continuous_on s ?inf" by (auto intro!: continuous_at_imp_continuous_on continuous_infdist continuous_ident) then obtain x where x: "x \ s" "\y\s. ?inf x \ ?inf y" using continuous_attains_inf[OF \compact s\ \s \ {}\] by auto then have "0 < ?inf x" using t \t \ {}\ in_closed_iff_infdist_zero by (auto simp: less_le infdist_nonneg) moreover have "\x'\s. \y\t. ?inf x \ dist x' y" using x by (auto intro: order_trans infdist_le) ultimately show ?thesis by auto qed (auto intro!: exI[of _ 1]) proposition separate_closed_compact: fixes s t :: "'a::heine_borel set" assumes "closed s" and "compact t" and "s \ t = {}" shows "\d>0. \x\s. \y\t. d \ dist x y" proof - have *: "t \ s = {}" using assms(3) by auto show ?thesis using separate_compact_closed[OF assms(2,1) *] by (force simp: dist_commute) qed proposition compact_in_open_separated: fixes A::"'a::heine_borel set" assumes "A \ {}" assumes "compact A" assumes "open B" assumes "A \ B" obtains e where "e > 0" "{x. infdist x A \ e} \ B" proof atomize_elim have "closed (- B)" "compact A" "- B \ A = {}" using assms by (auto simp: open_Diff compact_eq_bounded_closed) from separate_closed_compact[OF this] obtain d'::real where d': "d'>0" "\x y. x \ B \ y \ A \ d' \ dist x y" by auto define d where "d = d' / 2" hence "d>0" "d < d'" using d' by auto with d' have d: "\x y. x \ B \ y \ A \ d < dist x y" by force show "\e>0. {x. infdist x A \ e} \ B" proof (rule ccontr) assume "\e. 0 < e \ {x. infdist x A \ e} \ B" with \d > 0\ obtain x where x: "infdist x A \ d" "x \ B" by auto from assms have "closed A" "A \ {}" by (auto simp: compact_eq_bounded_closed) from infdist_attains_inf[OF this] obtain y where y: "y \ A" "infdist x A = dist x y" by auto have "dist x y \ d" using x y by simp also have "\ < dist x y" using y d x by auto finally show False by simp qed qed subsection \Uniform Continuity\ lemma uniformly_continuous_onE: assumes "uniformly_continuous_on s f" "0 < e" obtains d where "d>0" "\x x'. \x\s; x'\s; dist x' x < d\ \ dist (f x') (f x) < e" using assms by (auto simp: uniformly_continuous_on_def) lemma uniformly_continuous_on_sequentially: "uniformly_continuous_on s f \ (\x y. (\n. x n \ s) \ (\n. y n \ s) \ (\n. dist (x n) (y n)) \ 0 \ (\n. dist (f(x n)) (f(y n))) \ 0)" (is "?lhs = ?rhs") proof assume ?lhs { fix x y assume x: "\n. x n \ s" and y: "\n. y n \ s" and xy: "((\n. dist (x n) (y n)) \ 0) sequentially" { fix e :: real assume "e > 0" then obtain d where "d > 0" and d: "\x\s. \x'\s. dist x' x < d \ dist (f x') (f x) < e" using \?lhs\[unfolded uniformly_continuous_on_def, THEN spec[where x=e]] by auto obtain N where N: "\n\N. dist (x n) (y n) < d" using xy[unfolded lim_sequentially dist_norm] and \d>0\ by auto { fix n assume "n\N" then have "dist (f (x n)) (f (y n)) < e" using N[THEN spec[where x=n]] using d[THEN bspec[where x="x n"], THEN bspec[where x="y n"]] using x and y by (simp add: dist_commute) } then have "\N. \n\N. dist (f (x n)) (f (y n)) < e" by auto } then have "((\n. dist (f(x n)) (f(y n))) \ 0) sequentially" unfolding lim_sequentially and dist_real_def by auto } then show ?rhs by auto next assume ?rhs { assume "\ ?lhs" then obtain e where "e > 0" "\d>0. \x\s. \x'\s. dist x' x < d \ \ dist (f x') (f x) < e" unfolding uniformly_continuous_on_def by auto then obtain fa where fa: "\x. 0 < x \ fst (fa x) \ s \ snd (fa x) \ s \ dist (fst (fa x)) (snd (fa x)) < x \ \ dist (f (fst (fa x))) (f (snd (fa x))) < e" using choice[of "\d x. d>0 \ fst x \ s \ snd x \ s \ dist (snd x) (fst x) < d \ \ dist (f (snd x)) (f (fst x)) < e"] unfolding Bex_def by (auto simp: dist_commute) define x where "x n = fst (fa (inverse (real n + 1)))" for n define y where "y n = snd (fa (inverse (real n + 1)))" for n have xyn: "\n. x n \ s \ y n \ s" and xy0: "\n. dist (x n) (y n) < inverse (real n + 1)" and fxy:"\n. \ dist (f (x n)) (f (y n)) < e" unfolding x_def and y_def using fa by auto { fix e :: real assume "e > 0" then obtain N :: nat where "N \ 0" and N: "0 < inverse (real N) \ inverse (real N) < e" unfolding real_arch_inverse[of e] by auto { fix n :: nat assume "n \ N" then have "inverse (real n + 1) < inverse (real N)" using of_nat_0_le_iff and \N\0\ by auto also have "\ < e" using N by auto finally have "inverse (real n + 1) < e" by auto then have "dist (x n) (y n) < e" using xy0[THEN spec[where x=n]] by auto } then have "\N. \n\N. dist (x n) (y n) < e" by auto } then have "\e>0. \N. \n\N. dist (f (x n)) (f (y n)) < e" using \?rhs\[THEN spec[where x=x], THEN spec[where x=y]] and xyn unfolding lim_sequentially dist_real_def by auto then have False using fxy and \e>0\ by auto } then show ?lhs unfolding uniformly_continuous_on_def by blast qed subsection \Continuity on a Compact Domain Implies Uniform Continuity\ text\From the proof of the Heine-Borel theorem: Lemma 2 in section 3.7, page 69 of J. C. Burkill and H. Burkill. A Second Course in Mathematical Analysis (CUP, 2002)\ lemma Heine_Borel_lemma: assumes "compact S" and Ssub: "S \ \\" and opn: "\G. G \ \ \ open G" obtains e where "0 < e" "\x. x \ S \ \G \ \. ball x e \ G" proof - have False if neg: "\e. 0 < e \ \x \ S. \G \ \. \ ball x e \ G" proof - have "\x \ S. \G \ \. \ ball x (1 / Suc n) \ G" for n using neg by simp then obtain f where "\n. f n \ S" and fG: "\G n. G \ \ \ \ ball (f n) (1 / Suc n) \ G" by metis then obtain l r where "l \ S" "strict_mono r" and to_l: "(f \ r) \ l" using \compact S\ compact_def that by metis then obtain G where "l \ G" "G \ \" using Ssub by auto then obtain e where "0 < e" and e: "\z. dist z l < e \ z \ G" using opn open_dist by blast obtain N1 where N1: "\n. n \ N1 \ dist (f (r n)) l < e/2" using to_l apply (simp add: lim_sequentially) using \0 < e\ half_gt_zero that by blast obtain N2 where N2: "of_nat N2 > 2/e" using reals_Archimedean2 by blast obtain x where "x \ ball (f (r (max N1 N2))) (1 / real (Suc (r (max N1 N2))))" and "x \ G" using fG [OF \G \ \\, of "r (max N1 N2)"] by blast then have "dist (f (r (max N1 N2))) x < 1 / real (Suc (r (max N1 N2)))" by simp also have "... \ 1 / real (Suc (max N1 N2))" apply (simp add: field_split_simps del: max.bounded_iff) using \strict_mono r\ seq_suble by blast also have "... \ 1 / real (Suc N2)" by (simp add: field_simps) also have "... < e/2" using N2 \0 < e\ by (simp add: field_simps) - finally have "dist (f (r (max N1 N2))) x < e / 2" . + finally have "dist (f (r (max N1 N2))) x < e/2" . moreover have "dist (f (r (max N1 N2))) l < e/2" using N1 max.cobounded1 by blast ultimately have "dist x l < e" by metric then show ?thesis using e \x \ G\ by blast qed then show ?thesis by (meson that) qed lemma compact_uniformly_equicontinuous: assumes "compact S" and cont: "\x e. \x \ S; 0 < e\ \ \d. 0 < d \ (\f \ \. \x' \ S. dist x' x < d \ dist (f x') (f x) < e)" and "0 < e" obtains d where "0 < d" "\f x x'. \f \ \; x \ S; x' \ S; dist x' x < d\ \ dist (f x') (f x) < e" proof - obtain d where d_pos: "\x e. \x \ S; 0 < e\ \ 0 < d x e" and d_dist : "\x x' e f. \dist x' x < d x e; x \ S; x' \ S; 0 < e; f \ \\ \ dist (f x') (f x) < e" using cont by metis - let ?\ = "((\x. ball x (d x (e / 2))) ` S)" + let ?\ = "((\x. ball x (d x (e/2))) ` S)" have Ssub: "S \ \ ?\" by clarsimp (metis d_pos \0 < e\ dist_self half_gt_zero_iff) then obtain k where "0 < k" and k: "\x. x \ S \ \G \ ?\. ball x k \ G" by (rule Heine_Borel_lemma [OF \compact S\]) auto moreover have "dist (f v) (f u) < e" if "f \ \" "u \ S" "v \ S" "dist v u < k" for f u v proof - obtain G where "G \ ?\" "u \ G" "v \ G" using k that by (metis \dist v u < k\ \u \ S\ \0 < k\ centre_in_ball subsetD dist_commute mem_ball) - then obtain w where w: "dist w u < d w (e / 2)" "dist w v < d w (e / 2)" "w \ S" + then obtain w where w: "dist w u < d w (e/2)" "dist w v < d w (e/2)" "w \ S" by auto with that d_dist have "dist (f w) (f v) < e/2" by (metis \0 < e\ dist_commute half_gt_zero) moreover have "dist (f w) (f u) < e/2" using that d_dist w by (metis \0 < e\ dist_commute divide_pos_pos zero_less_numeral) ultimately show ?thesis using dist_triangle_half_r by blast qed ultimately show ?thesis using that by blast qed corollary compact_uniformly_continuous: fixes f :: "'a :: metric_space \ 'b :: metric_space" assumes f: "continuous_on S f" and S: "compact S" shows "uniformly_continuous_on S f" using f unfolding continuous_on_iff uniformly_continuous_on_def by (force intro: compact_uniformly_equicontinuous [OF S, of "{f}"]) subsection\<^marker>\tag unimportant\\ Theorems relating continuity and uniform continuity to closures\ lemma continuous_on_closure: "continuous_on (closure S) f \ (\x e. x \ closure S \ 0 < e \ (\d. 0 < d \ (\y. y \ S \ dist y x < d \ 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 \ closure S" obtain \::real where "\ > 0" and \: "\y. \y \ S; dist y x < \\ \ dist (f y) (f x) < e/2" using R [of x "e/2"] \0 < e\ x by auto have "dist (f y) (f x) \ e" if y: "y \ closure S" and dyx: "dist y x < \/2" for y proof - obtain \'::real where "\' > 0" and \': "\z. \z \ S; dist z y < \'\ \ dist (f z) (f y) < e/2" using R [of y "e/2"] \0 < e\ y by auto obtain z where "z \ S" and z: "dist z y < min \' \ / 2" using closure_approachable y by (metis \0 < \'\ \0 < \\ divide_pos_pos min_less_iff_conj zero_less_numeral) have "dist (f z) (f y) < e/2" using \' [OF \z \ S\] z \0 < \'\ by metric moreover have "dist (f z) (f x) < e/2" using \[OF \z \ S\] z dyx by metric ultimately show ?thesis by metric qed then show "\d>0. \x'\closure S. dist x' x < d \ dist (f x') (f x) \ e" by (rule_tac x="\/2" in exI) (simp add: \\ > 0\) qed qed lemma continuous_on_closure_sequentially: fixes f :: "'a::metric_space \ 'b :: metric_space" shows "continuous_on (closure S) f \ (\x a. a \ closure S \ (\n. x n \ S) \ x \ a \ (f \ x) \ f a)" (is "?lhs = ?rhs") proof - have "continuous_on (closure S) f \ (\x \ 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 \ '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: "\x x'. \x\S; x'\S; dist x' x < d\ \ dist (f x') (f x) < e/3" using ucont [unfolded uniformly_continuous_on_def, rule_format, of "e/3"] by auto show "\d>0. \x\closure S. \x'\closure S. dist x' x < d \ dist (f x') (f x) < e" proof (rule exI [where x="d/3"], clarsimp simp: \d > 0\) fix x y assume x: "x \ closure S" and y: "y \ closure S" and dyx: "dist y x * 3 < d" obtain d1::real where "d1 > 0" and d1: "\w. \w \ closure S; dist w x < d1\ \ dist (f w) (f x) < e/3" using cont [unfolded continuous_on_iff, rule_format, of "x" "e/3"] \0 < e\ x by auto obtain x' where "x' \ S" and x': "dist x' x < min d1 (d / 3)" using closure_approachable [of x S] by (metis \0 < d1\ \0 < d\ divide_pos_pos min_less_iff_conj x zero_less_numeral) obtain d2::real where "d2 > 0" and d2: "\w \ closure S. dist w y < d2 \ dist (f w) (f y) < e/3" using cont [unfolded continuous_on_iff, rule_format, of "y" "e/3"] \0 < e\ y by auto obtain y' where "y' \ S" and y': "dist y' y < min d2 (d / 3)" using closure_approachable [of y S] by (metis \0 < d2\ \0 < d\ divide_pos_pos min_less_iff_conj y zero_less_numeral) have "dist x' x < d/3" using x' by auto then have "dist x' y' < d" using dyx y' by metric then have "dist (f x') (f y') < e/3" by (rule d [OF \y' \ S\ \x' \ S\]) moreover have "dist (f x') (f x) < e/3" using \x' \ S\ closure_subset x' d1 by (simp add: closure_def) moreover have "dist (f y') (f y) < e/3" using \y' \ S\ closure_subset y' d2 by (simp add: closure_def) ultimately show "dist (f y) (f x) < e" by metric qed qed lemma uniformly_continuous_on_extension_at_closure: fixes f::"'a::metric_space \ 'b::complete_space" assumes uc: "uniformly_continuous_on X f" assumes "x \ closure X" obtains l where "(f \ l) (at x within X)" proof - from assms obtain xs where xs: "xs \ x" "\n. xs n \ X" by (auto simp: closure_sequential) from uniformly_continuous_on_Cauchy[OF uc LIMSEQ_imp_Cauchy, OF xs] obtain l where l: "(\n. f (xs n)) \ l" by atomize_elim (simp only: convergent_eq_Cauchy) have "(f \ l) (at x within X)" proof (safe intro!: Lim_within_LIMSEQ) fix xs' assume "\n. xs' n \ x \ xs' n \ X" and xs': "xs' \ x" then have "xs' n \ x" "xs' n \ X" for n by auto from uniformly_continuous_on_Cauchy[OF uc LIMSEQ_imp_Cauchy, OF \xs' \ x\ \xs' _ \ X\] obtain l' where l': "(\n. f (xs' n)) \ l'" by atomize_elim (simp only: convergent_eq_Cauchy) show "(\n. f (xs' n)) \ l" proof (rule tendstoI) fix e::real assume "e > 0" - define e' where "e' \ e / 2" + define e' where "e' \ e/2" have "e' > 0" using \e > 0\ by (simp add: e'_def) have "\\<^sub>F n in sequentially. dist (f (xs n)) l < e'" by (simp add: \0 < e'\ l tendstoD) moreover from uc[unfolded uniformly_continuous_on_def, rule_format, OF \e' > 0\] obtain d where d: "d > 0" "\x x'. x \ X \ x' \ X \ dist x x' < d \ dist (f x) (f x') < e'" by auto have "\\<^sub>F n in sequentially. dist (xs n) (xs' n) < d" by (auto intro!: \0 < d\ order_tendstoD tendsto_eq_intros xs xs') ultimately show "\\<^sub>F n in sequentially. dist (f (xs' n)) l < e" proof eventually_elim case (elim n) have "dist (f (xs' n)) l \ dist (f (xs n)) (f (xs' n)) + dist (f (xs n)) l" by metric also have "dist (f (xs n)) (f (xs' n)) < e'" by (auto intro!: d xs \xs' _ \ _\ elim) also note \dist (f (xs n)) l < e'\ 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 \ 'b::complete_space" assumes uc: "uniformly_continuous_on X f" obtains g where "uniformly_continuous_on (closure X) g" "\x. x \ X \ f x = g x" "\Y h x. X \ Y \ Y \ closure X \ continuous_on Y h \ (\x. x \ X \ f x = h x) \ x \ Y \ 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 \ y x) (at x within X)" if "x \ closure X" for x apply atomize_elim apply (rule choice) using uniformly_continuous_on_extension_at_closure[OF assms] by metis let ?g = "\x. if x \ 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' \ e / 3" have "e' > 0" using \e > 0\ by (simp add: e'_def) from uc[unfolded uniformly_continuous_on_def, rule_format, OF \0 < e'\] obtain d where "d > 0" and d: "\x x'. x \ X \ x' \ X \ dist x' x < d \ dist (f x') (f x) < e'" by auto define d' where "d' = d / 3" have "d' > 0" using \d > 0\ by (simp add: d'_def) show "\d>0. \x\closure X. \x'\closure X. dist x' x < d \ dist (?g x') (?g x) < e" proof (safe intro!: exI[where x=d'] \d' > 0\) fix x x' assume x: "x \ closure X" and x': "x' \ closure X" and dist: "dist x' x < d'" then obtain xs xs' where xs: "xs \ x" "\n. xs n \ X" and xs': "xs' \ x'" "\n. xs' n \ X" by (auto simp: closure_sequential) have "\\<^sub>F n in sequentially. dist (xs' n) x' < d'" and "\\<^sub>F n in sequentially. dist (xs n) x < d'" by (auto intro!: \0 < d'\ order_tendstoD tendsto_eq_intros xs xs') moreover have "(\x. f (xs x)) \ y x" if "x \ closure X" "x \ X" "xs \ x" "\n. xs n \ X" for xs x using that not_eventuallyD by (force intro!: filterlim_compose[OF y[OF \x \ closure X\]] simp: filterlim_at) then have "(\x. f (xs' x)) \ ?g x'" "(\x. f (xs x)) \ ?g x" using x x' by (auto intro!: continuous_on_tendsto_compose[OF cont_f] simp: xs' xs) then have "\\<^sub>F n in sequentially. dist (f (xs' n)) (?g x') < e'" "\\<^sub>F n in sequentially. dist (f (xs n)) (?g x) < e'" by (auto intro!: \0 < e'\ order_tendstoD tendsto_eq_intros) ultimately have "\\<^sub>F n in sequentially. dist (?g x') (?g x) < e" proof eventually_elim case (elim n) have "dist (?g x') (?g x) \ 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 from \dist (xs' n) x' < d'\ \dist x' x < d'\ \dist (xs n) x < d'\ have "dist (xs' n) (xs n) < d" unfolding d'_def by metric with \xs _ \ X\ \xs' _ \ X\ have "dist (f (xs' n)) (f (xs n)) < e'" by (rule d) also note \dist (f (xs' n)) (?g x') < e'\ also note \dist (f (xs n)) (?g x) < e'\ 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 \ X" for x using that by simp moreover { fix Y h x assume Y: "x \ Y" "X \ Y" "Y \ closure X" and cont_h: "continuous_on Y h" and extension: "(\x. x \ X \ f x = h x)" { assume "x \ X" have "x \ closure X" using Y by auto then obtain xs where xs: "xs \ x" "\n. xs n \ X" by (auto simp: closure_sequential) from continuous_on_tendsto_compose[OF cont_h xs(1)] xs(2) Y have hx: "(\x. f (xs x)) \ h x" by (auto simp: subsetD extension) then have "(\x. f (xs x)) \ y x" using \x \ X\ not_eventuallyD xs(2) by (force intro!: filterlim_compose[OF y[OF \x \ closure X\]] 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 \ '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 \With Abstract Topology (TODO: move and remove dependency?)\ lemma openin_contains_ball: "openin (top_of_set t) s \ s \ t \ (\x \ s. \e. 0 < e \ ball x e \ t \ s)" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs apply (simp add: openin_open) apply (metis Int_commute Int_mono inf.cobounded2 open_contains_ball order_refl subsetCE) done next assume ?rhs then show ?lhs apply (simp add: openin_euclidean_subtopology_iff) by (metis (no_types) Int_iff dist_commute inf.absorb_iff2 mem_ball) qed lemma openin_contains_cball: "openin (top_of_set t) s \ s \ t \ (\x \ s. \e. 0 < e \ cball x e \ t \ s)" apply (simp add: openin_contains_ball) apply (rule iffI) apply (auto dest!: bspec) apply (rule_tac x="e/2" in exI, force+) done subsection \Closed Nest\ text \Bounded closed nest property (proof does not use Heine-Borel)\ lemma bounded_closed_nest: fixes S :: "nat \ ('a::heine_borel) set" assumes "\n. closed (S n)" and "\n. S n \ {}" and "\m n. m \ n \ S n \ S m" and "bounded (S 0)" obtains a where "\n. a \ S n" proof - from assms(2) obtain x where x: "\n. x n \ S n" using choice[of "\n x. x \ 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 \ S 0" "strict_mono r" "(x \ r) \ l" using x and assms(3) unfolding seq_compact_def by blast have "\n. l \ S n" proof fix n :: nat have "closed (S n)" using assms(1) by simp moreover have "\i. (x \ r) i \ S i" using x and assms(3) and lr(2) [THEN seq_suble] by auto then have "\i. (x \ r) (i + n) \ S n" using assms(3) by (fast intro!: le_add2) moreover have "(\i. (x \ r) (i + n)) \ l" using lr(3) by (rule LIMSEQ_ignore_initial_segment) ultimately show "l \ S n" by (rule closed_sequentially) qed then show ?thesis using that by blast qed text \Decreasing case does not even need compactness, just completeness.\ lemma decreasing_closed_nest: fixes S :: "nat \ ('a::complete_space) set" assumes "\n. closed (S n)" "\n. S n \ {}" "\m n. m \ n \ S n \ S m" "\e. e>0 \ \n. \x\S n. \y\S n. dist x y < e" obtains a where "\n. a \ S n" proof - have "\n. \x. x \ S n" using assms(2) by auto then have "\t. \n. t n \ S n" using choice[of "\n x. x \ S n"] by auto then obtain t where t: "\n. t n \ S n" by auto { fix e :: real assume "e > 0" then obtain N where N: "\x\S N. \y\S N. dist x y < e" using assms(4) by blast { fix m n :: nat assume "N \ m \ N \ n" then have "t m \ S N" "t n \ 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 "\N. \m n. N \ m \ N \ n \ dist (t m) (t n) < e" by auto } then have "Cauchy t" unfolding cauchy_def by auto then obtain l where l:"(t \ 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: "\n\N. dist (t n) l < e" using l[unfolded lim_sequentially] by auto have "t (max n N) \ S n" by (meson assms(3) contra_subsetD max.cobounded1 t) then have "\y\S n. dist y l < e" using N max.cobounded2 by blast } then have "l \ S n" using closed_approachable[of "S n" l] assms(1) by auto } then show ?thesis using that by blast qed text \Strengthen it to the intersection actually being a singleton.\ lemma decreasing_closed_nest_sing: fixes S :: "nat \ 'a::complete_space set" assumes "\n. closed(S n)" "\n. S n \ {}" "\m n. m \ n \ S n \ S m" "\e. e>0 \ \n. \x \ (S n). \ y\(S n). dist x y < e" shows "\a. \(range S) = {a}" proof - obtain a where a: "\n. a \ S n" using decreasing_closed_nest[of S] using assms by auto { fix b assume b: "b \ \(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 "\(range S) = {a}" unfolding image_def by auto then show ?thesis .. qed subsection\<^marker>\tag unimportant\ \Making a continuous function avoid some value in a neighbourhood\ lemma continuous_within_avoid: fixes f :: "'a::metric_space \ 'b::t1_space" assumes "continuous (at x within s) f" and "f x \ a" shows "\e>0. \y \ s. dist x y < e --> f y \ a" proof - obtain U where "open U" and "f x \ U" and "a \ U" using t1_space [OF \f x \ a\] by fast have "(f \ f x) (at x within s)" using assms(1) by (simp add: continuous_within) then have "eventually (\y. f y \ U) (at x within s)" using \open U\ and \f x \ U\ unfolding tendsto_def by fast then have "eventually (\y. f y \ a) (at x within s)" using \a \ U\ by (fast elim: eventually_mono) then show ?thesis using \f x \ a\ by (auto simp: dist_commute eventually_at) qed lemma continuous_at_avoid: fixes f :: "'a::metric_space \ 'b::t1_space" assumes "continuous (at x) f" and "f x \ a" shows "\e>0. \y. dist x y < e \ f y \ a" using assms continuous_within_avoid[of x UNIV f a] by simp lemma continuous_on_avoid: fixes f :: "'a::metric_space \ 'b::t1_space" assumes "continuous_on s f" and "x \ s" and "f x \ a" shows "\e>0. \y \ s. dist x y < e \ f y \ 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 \ 'b::t1_space" assumes "continuous_on s f" and "open s" and "x \ s" and "f x \ a" shows "\e>0. \y. dist x y < e \ f y \ 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 \Consequences for Real Numbers\ lemma closed_contains_Inf: fixes S :: "real set" shows "S \ {} \ bdd_below S \ closed S \ Inf S \ S" by (metis closure_contains_Inf closure_closed) lemma closed_subset_contains_Inf: fixes A C :: "real set" shows "closed C \ A \ C \ A \ {} \ bdd_below A \ Inf A \ C" by (metis closure_contains_Inf closure_minimal subset_eq) lemma closed_contains_Sup: fixes S :: "real set" shows "S \ {} \ bdd_above S \ closed S \ Sup S \ S" by (subst closure_closed[symmetric], assumption, rule closure_contains_Sup) lemma closed_subset_contains_Sup: fixes A C :: "real set" shows "closed C \ A \ C \ A \ {} \ bdd_above A \ Sup A \ C" by (metis closure_contains_Sup closure_minimal subset_eq) lemma atLeastAtMost_subset_contains_Inf: fixes A :: "real set" and a b :: real shows "A \ {} \ a \ b \ A \ {a..b} \ Inf A \ {a..b}" by (rule closed_subset_contains_Inf) (auto intro: closed_real_atLeastAtMost intro!: bdd_belowI[of A a]) lemma bounded_real: "bounded (S::real set) \ (\a. \x\S. \x\ \ a)" by (simp add: bounded_iff) lemma bounded_imp_bdd_above: "bounded S \ 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 \ 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 \ {}" shows "\x\S. x \ Sup S" and "\b. (\x\S. x \ b) \ Sup S \ b" proof show "\b. (\x\S. x \ b) \ Sup S \ 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 \ 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 \ {}" shows "\x\S. x \ Inf S" and "\b. (\x\S. x \ b) \ Inf S \ b" proof show "\b. (\x\S. x \ b) \ Inf S \ 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 \ 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 open_real: fixes s :: "real set" shows "open s \ (\x \ s. \e>0. \x'. \x' - x\ < e --> x' \ s)" unfolding open_dist dist_norm by simp lemma islimpt_approachable_real: fixes s :: "real set" shows "x islimpt s \ (\e>0. \x'\ s. x' \ x \ \x' - x\ < e)" unfolding islimpt_approachable dist_norm by simp lemma closed_real: fixes s :: "real set" shows "closed s \ (\x. (\e>0. \x' \ s. x' \ x \ \x' - x\ < e) \ x \ s)" unfolding closed_limpt islimpt_approachable dist_norm by simp lemma continuous_at_real_range: fixes f :: "'a::real_normed_vector \ real" shows "continuous (at x) f \ (\e>0. \d>0. \x'. norm(x' - x) < d --> \f x' - f x\ < e)" unfolding continuous_at unfolding Lim_at unfolding dist_norm apply auto apply (erule_tac x=e in allE, auto) apply (rule_tac x=d in exI, auto) apply (erule_tac x=x' in allE, auto) apply (erule_tac x=e in allE, auto) done lemma continuous_on_real_range: fixes f :: "'a::real_normed_vector \ real" shows "continuous_on s f \ (\x \ s. \e>0. \d>0. (\x' \ s. norm(x' - x) < d \ \f x' - f x\ < e))" unfolding continuous_on_iff dist_norm by simp lemma continuous_on_closed_Collect_le: fixes f g :: "'a::topological_space \ real" assumes f: "continuous_on s f" and g: "continuous_on s g" and s: "closed s" shows "closed {x \ s. f x \ g x}" proof - have "closed ((\x. g x - f x) -` {0..} \ s)" using closed_real_atLeast continuous_on_diff [OF g f] by (simp add: continuous_on_closed_vimage [OF s]) also have "((\x. g x - f x) -` {0..} \ s) = {x\s. f x \ g x}" by auto finally show ?thesis . qed lemma continuous_le_on_closure: fixes a::real assumes f: "continuous_on (closure s) f" and x: "x \ closure(s)" and xlo: "\x. x \ s ==> f(x) \ a" shows "f(x) \ a" using image_closure_subset [OF f, where T=" {x. x \ a}" ] assms continuous_on_closed_Collect_le[of "UNIV" "\x. x" "\x. a"] by auto lemma continuous_ge_on_closure: fixes a::real assumes f: "continuous_on (closure s) f" and x: "x \ closure(s)" and xlo: "\x. x \ s ==> f(x) \ a" shows "f(x) \ a" using image_closure_subset [OF f, where T=" {x. a \ x}"] assms continuous_on_closed_Collect_le[of "UNIV" "\x. a" "\x. x"] by auto subsection\The infimum of the distance between two sets\ definition\<^marker>\tag important\ setdist :: "'a::metric_space set \ 'a set \ real" where "setdist s t \ (if s = {} \ t = {} then 0 else Inf {dist x y| x y. x \ s \ y \ t})" lemma setdist_empty1 [simp]: "setdist {} t = 0" by (simp add: setdist_def) lemma setdist_empty2 [simp]: "setdist t {} = 0" by (simp add: setdist_def) lemma setdist_pos_le [simp]: "0 \ setdist s t" by (auto simp: setdist_def ex_in_conv [symmetric] intro: cInf_greatest) lemma le_setdistI: assumes "s \ {}" "t \ {}" "\x y. \x \ s; y \ t\ \ d \ dist x y" shows "d \ setdist s t" using assms by (auto simp: setdist_def Set.ex_in_conv [symmetric] intro: cInf_greatest) lemma setdist_le_dist: "\x \ s; y \ t\ \ setdist s t \ dist x y" unfolding setdist_def by (auto intro!: bdd_belowI [where m=0] cInf_lower) lemma le_setdist_iff: "d \ setdist s t \ (\x \ s. \y \ t. d \ dist x y) \ (s = {} \ t = {} \ d \ 0)" apply (cases "s = {} \ t = {}") apply (force simp add: setdist_def) apply (intro iffI conjI) using setdist_le_dist apply fastforce apply (auto simp: intro: le_setdistI) done lemma setdist_ltE: assumes "setdist s t < b" "s \ {}" "t \ {}" obtains x y where "x \ s" "y \ t" "dist x y < b" using assms by (auto simp: not_le [symmetric] le_setdist_iff) lemma setdist_refl: "setdist s s = 0" apply (cases "s = {}") apply (force simp add: setdist_def) apply (rule antisym [OF _ setdist_pos_le]) apply (metis all_not_in_conv dist_self setdist_le_dist) done lemma setdist_sym: "setdist s t = setdist t s" by (force simp: setdist_def dist_commute intro!: arg_cong [where f=Inf]) lemma setdist_triangle: "setdist s t \ setdist s {a} + setdist {a} t" proof (cases "s = {} \ t = {}") case True then show ?thesis using setdist_pos_le by fastforce next case False have "\x. x \ s \ setdist s t - dist x a \ setdist {a} t" apply (rule le_setdistI, blast) using False apply (fastforce intro: le_setdistI) apply (simp add: algebra_simps) apply (metis dist_commute dist_triangle3 order_trans [OF setdist_le_dist]) done then have "setdist s t - setdist {a} t \ setdist s {a}" using False by (fastforce intro: le_setdistI) then show ?thesis by (simp add: algebra_simps) qed lemma setdist_singletons [simp]: "setdist {x} {y} = dist x y" by (simp add: setdist_def) lemma setdist_Lipschitz: "\setdist {x} s - setdist {y} s\ \ dist x y" apply (subst setdist_singletons [symmetric]) by (metis abs_diff_le_iff diff_le_eq setdist_triangle setdist_sym) lemma continuous_at_setdist [continuous_intros]: "continuous (at x) (\y. (setdist {y} s))" by (force simp: continuous_at_eps_delta dist_real_def intro: le_less_trans [OF setdist_Lipschitz]) lemma continuous_on_setdist [continuous_intros]: "continuous_on t (\y. (setdist {y} s))" by (metis continuous_at_setdist continuous_at_imp_continuous_on) lemma uniformly_continuous_on_setdist: "uniformly_continuous_on t (\y. (setdist {y} s))" by (force simp: uniformly_continuous_on_def dist_real_def intro: le_less_trans [OF setdist_Lipschitz]) lemma setdist_subset_right: "\t \ {}; t \ u\ \ setdist s u \ setdist s t" apply (cases "s = {} \ u = {}", force) apply (auto simp: setdist_def intro!: bdd_belowI [where m=0] cInf_superset_mono) done lemma setdist_subset_left: "\s \ {}; s \ t\ \ setdist t u \ setdist s u" by (metis setdist_subset_right setdist_sym) lemma setdist_closure_1 [simp]: "setdist (closure s) t = setdist s t" proof (cases "s = {} \ t = {}") case True then show ?thesis by force next case False { fix y assume "y \ t" have "continuous_on (closure s) (\a. dist a y)" by (auto simp: continuous_intros dist_norm) then have *: "\x. x \ closure s \ setdist s t \ dist x y" apply (rule continuous_ge_on_closure) apply assumption apply (blast intro: setdist_le_dist \y \ t\ ) done } note * = this show ?thesis apply (rule antisym) using False closure_subset apply (blast intro: setdist_subset_left) using False * apply (force intro!: le_setdistI) done qed lemma setdist_closure_2 [simp]: "setdist t (closure s) = setdist t s" by (metis setdist_closure_1 setdist_sym) lemma setdist_eq_0I: "\x \ S; x \ T\ \ setdist S T = 0" by (metis antisym dist_self setdist_le_dist setdist_pos_le) lemma setdist_unique: "\a \ S; b \ T; \x y. x \ S \ y \ T ==> dist a b \ dist x y\ \ setdist S T = dist a b" by (force simp add: setdist_le_dist le_setdist_iff intro: antisym) lemma setdist_le_sing: "x \ S ==> setdist S T \ setdist {x} T" using setdist_subset_left by auto lemma infdist_eq_setdist: "infdist x A = setdist {x} A" by (simp add: infdist_def setdist_def Setcompr_eq_image) lemma setdist_eq_infdist: "setdist A B = (if A = {} then 0 else INF a\A. infdist a B)" proof - have "Inf {dist x y |x y. x \ A \ y \ B} = (INF x\A. Inf (dist x ` B))" if "b \ B" "a \ A" for a b proof (rule order_antisym) have "Inf {dist x y |x y. x \ A \ y \ B} \ Inf (dist x ` B)" if "b \ B" "a \ A" "x \ A" for x proof - have *: "\b'. b' \ B \ Inf {dist x y |x y. x \ A \ y \ B} \ dist x b'" by (metis (mono_tags, lifting) ex_in_conv setdist_def setdist_le_dist that(3)) show ?thesis using that by (subst conditionally_complete_lattice_class.le_cInf_iff) (auto simp: *)+ qed then show "Inf {dist x y |x y. x \ A \ y \ B} \ (INF x\A. Inf (dist x ` B))" using that by (subst conditionally_complete_lattice_class.le_cInf_iff) (auto simp: bdd_below_def) next have *: "\x y. \b \ B; a \ A; x \ A; y \ B\ \ \a\A. Inf (dist a ` B) \ dist x y" by (meson bdd_below_image_dist cINF_lower) show "(INF x\A. Inf (dist x ` B)) \ Inf {dist x y |x y. x \ A \ y \ B}" proof (rule conditionally_complete_lattice_class.cInf_mono) show "bdd_below ((\x. Inf (dist x ` B)) ` A)" by (metis (no_types, lifting) bdd_belowI2 ex_in_conv infdist_def infdist_nonneg that(1)) qed (use that in \auto simp: *\) qed then show ?thesis by (auto simp: setdist_def infdist_def) qed lemma infdist_mono: assumes "A \ B" "A \ {}" shows "infdist x B \ infdist x A" by (simp add: assms infdist_eq_setdist setdist_subset_right) lemma infdist_singleton [simp]: "infdist x {y} = dist x y" by (simp add: infdist_eq_setdist) proposition setdist_attains_inf: assumes "compact B" "B \ {}" obtains y where "y \ B" "setdist A B = infdist y A" proof (cases "A = {}") case True then show thesis by (metis assms diameter_compact_attained infdist_def setdist_def that) next case False obtain y where "y \ B" and min: "\y'. y' \ B \ infdist y A \ infdist y' A" by (metis continuous_attains_inf [OF assms continuous_on_infdist] continuous_on_id) show thesis proof have "setdist A B = (INF y\B. infdist y A)" by (metis \B \ {}\ setdist_eq_infdist setdist_sym) also have "\ = infdist y A" proof (rule order_antisym) show "(INF y\B. infdist y A) \ infdist y A" proof (rule cInf_lower) show "infdist y A \ (\y. infdist y A) ` B" using \y \ B\ by blast show "bdd_below ((\y. infdist y A) ` B)" by (meson bdd_belowI2 infdist_nonneg) qed next show "infdist y A \ (INF y\B. infdist y A)" by (simp add: \B \ {}\ cINF_greatest min) qed finally show "setdist A B = infdist y A" . qed (fact \y \ B\) qed end diff --git a/src/HOL/Analysis/Elementary_Topology.thy b/src/HOL/Analysis/Elementary_Topology.thy --- a/src/HOL/Analysis/Elementary_Topology.thy +++ b/src/HOL/Analysis/Elementary_Topology.thy @@ -1,2693 +1,2686 @@ (* Author: L C Paulson, University of Cambridge Author: Amine Chaieb, University of Cambridge Author: Robert Himmelmann, TU Muenchen Author: Brian Huffman, Portland State University *) chapter \Topology\ theory Elementary_Topology imports "HOL-Library.Set_Idioms" "HOL-Library.Disjoint_Sets" Product_Vector begin section \Elementary Topology\ subsubsection\<^marker>\tag unimportant\ \Affine transformations of intervals\ lemma real_affinity_le: "0 < m \ m * x + c \ y \ x \ inverse m * y + - (c / m)" for m :: "'a::linordered_field" by (simp add: field_simps) lemma real_le_affinity: "0 < m \ y \ m * x + c \ inverse m * y + - (c / m) \ x" for m :: "'a::linordered_field" by (simp add: field_simps) lemma real_affinity_lt: "0 < m \ m * x + c < y \ x < inverse m * y + - (c / m)" for m :: "'a::linordered_field" by (simp add: field_simps) lemma real_lt_affinity: "0 < m \ y < m * x + c \ inverse m * y + - (c / m) < x" for m :: "'a::linordered_field" by (simp add: field_simps) lemma real_affinity_eq: "m \ 0 \ m * x + c = y \ x = inverse m * y + - (c / m)" for m :: "'a::linordered_field" by (simp add: field_simps) lemma real_eq_affinity: "m \ 0 \ y = m * x + c \ inverse m * y + - (c / m) = x" for m :: "'a::linordered_field" by (simp add: field_simps) subsection \Topological Basis\ context topological_space begin definition\<^marker>\tag important\ "topological_basis B \ (\b\B. open b) \ (\x. open x \ (\B'. B' \ B \ \B' = x))" lemma topological_basis: "topological_basis B \ (\x. open x \ (\B'. B' \ B \ \B' = x))" unfolding topological_basis_def apply safe apply fastforce apply fastforce apply (erule_tac x=x in allE, simp) apply (rule_tac x="{x}" in exI, auto) done lemma topological_basis_iff: assumes "\B'. B' \ B \ open B'" shows "topological_basis B \ (\O'. open O' \ (\x\O'. \B'\B. x \ B' \ B' \ O'))" (is "_ \ ?rhs") proof safe fix O' and x::'a assume H: "topological_basis B" "open O'" "x \ O'" then have "(\B'\B. \B' = O')" by (simp add: topological_basis_def) then obtain B' where "B' \ B" "O' = \B'" by auto then show "\B'\B. x \ B' \ B' \ O'" using H by auto next assume H: ?rhs show "topological_basis B" using assms unfolding topological_basis_def proof safe fix O' :: "'a set" assume "open O'" with H obtain f where "\x\O'. f x \ B \ x \ f x \ f x \ O'" by (force intro: bchoice simp: Bex_def) then show "\B'\B. \B' = O'" by (auto intro: exI[where x="{f x |x. x \ O'}"]) qed qed lemma topological_basisI: assumes "\B'. B' \ B \ open B'" and "\O' x. open O' \ x \ O' \ \B'\B. x \ B' \ B' \ O'" shows "topological_basis B" using assms by (subst topological_basis_iff) auto lemma topological_basisE: fixes O' assumes "topological_basis B" and "open O'" and "x \ O'" obtains B' where "B' \ B" "x \ B'" "B' \ O'" proof atomize_elim from assms have "\B'. B'\B \ open B'" by (simp add: topological_basis_def) with topological_basis_iff assms show "\B'. B' \ B \ x \ B' \ B' \ O'" using assms by (simp add: Bex_def) qed lemma topological_basis_open: assumes "topological_basis B" and "X \ B" shows "open X" using assms by (simp add: topological_basis_def) lemma topological_basis_imp_subbasis: assumes B: "topological_basis B" shows "open = generate_topology B" proof (intro ext iffI) fix S :: "'a set" assume "open S" with B obtain B' where "B' \ B" "S = \B'" unfolding topological_basis_def by blast then show "generate_topology B S" by (auto intro: generate_topology.intros dest: topological_basis_open) next fix S :: "'a set" assume "generate_topology B S" then show "open S" by induct (auto dest: topological_basis_open[OF B]) qed lemma basis_dense: fixes B :: "'a set set" and f :: "'a set \ 'a" assumes "topological_basis B" and choosefrom_basis: "\B'. B' \ {} \ f B' \ B'" shows "\X. open X \ X \ {} \ (\B' \ B. f B' \ X)" proof (intro allI impI) fix X :: "'a set" assume "open X" and "X \ {}" from topological_basisE[OF \topological_basis B\ \open X\ choosefrom_basis[OF \X \ {}\]] obtain B' where "B' \ B" "f X \ B'" "B' \ X" . then show "\B'\B. f B' \ X" by (auto intro!: choosefrom_basis) qed end lemma topological_basis_prod: assumes A: "topological_basis A" and B: "topological_basis B" shows "topological_basis ((\(a, b). a \ b) ` (A \ B))" unfolding topological_basis_def proof (safe, simp_all del: ex_simps add: subset_image_iff ex_simps(1)[symmetric]) fix S :: "('a \ 'b) set" assume "open S" then show "\X\A \ B. (\(a,b)\X. a \ b) = S" proof (safe intro!: exI[of _ "{x\A \ B. fst x \ snd x \ S}"]) fix x y assume "(x, y) \ S" from open_prod_elim[OF \open S\ this] obtain a b where a: "open a""x \ a" and b: "open b" "y \ b" and "a \ b \ S" by (metis mem_Sigma_iff) moreover from A a obtain A0 where "A0 \ A" "x \ A0" "A0 \ a" by (rule topological_basisE) moreover from B b obtain B0 where "B0 \ B" "y \ B0" "B0 \ b" by (rule topological_basisE) ultimately show "(x, y) \ (\(a, b)\{X \ A \ B. fst X \ snd X \ S}. a \ b)" by (intro UN_I[of "(A0, B0)"]) auto qed auto qed (metis A B topological_basis_open open_Times) subsection \Countable Basis\ locale\<^marker>\tag important\ countable_basis = topological_space p for p::"'a set \ bool" + fixes B :: "'a set set" assumes is_basis: "topological_basis B" and countable_basis: "countable B" begin lemma open_countable_basis_ex: assumes "p X" shows "\B' \ B. X = \B'" using assms countable_basis is_basis unfolding topological_basis_def by blast lemma open_countable_basisE: assumes "p X" obtains B' where "B' \ B" "X = \B'" using assms open_countable_basis_ex by atomize_elim simp lemma countable_dense_exists: "\D::'a set. countable D \ (\X. p X \ X \ {} \ (\d \ D. d \ X))" proof - let ?f = "(\B'. SOME x. x \ B')" have "countable (?f ` B)" using countable_basis by simp with basis_dense[OF is_basis, of ?f] show ?thesis by (intro exI[where x="?f ` B"]) (metis (mono_tags) all_not_in_conv imageI someI) qed lemma countable_dense_setE: obtains D :: "'a set" where "countable D" "\X. p X \ X \ {} \ \d \ D. d \ X" using countable_dense_exists by blast end lemma countable_basis_openI: "countable_basis open B" if "countable B" "topological_basis B" using that by unfold_locales (simp_all add: topological_basis topological_space.topological_basis topological_space_axioms) lemma (in first_countable_topology) first_countable_basisE: fixes x :: 'a obtains \ where "countable \" "\A. A \ \ \ x \ A" "\A. A \ \ \ open A" "\S. open S \ x \ S \ (\A\\. A \ S)" proof - obtain \ where \: "(\i::nat. x \ \ i \ open (\ i))" "(\S. open S \ x \ S \ (\i. \ i \ S))" using first_countable_basis[of x] by metis show thesis proof show "countable (range \)" by simp qed (use \ in auto) qed lemma (in first_countable_topology) first_countable_basis_Int_stableE: obtains \ where "countable \" "\A. A \ \ \ x \ A" "\A. A \ \ \ open A" "\S. open S \ x \ S \ (\A\\. A \ S)" "\A B. A \ \ \ B \ \ \ A \ B \ \" proof atomize_elim obtain \ where \: "countable \" "\B. B \ \ \ x \ B" "\B. B \ \ \ open B" "\S. open S \ x \ S \ \B\\. B \ S" by (rule first_countable_basisE) blast define \ where [abs_def]: "\ = (\N. \((\n. from_nat_into \ n) ` N)) ` (Collect finite::nat set set)" then show "\\. countable \ \ (\A. A \ \ \ x \ A) \ (\A. A \ \ \ open A) \ (\S. open S \ x \ S \ (\A\\. A \ S)) \ (\A B. A \ \ \ B \ \ \ A \ B \ \)" proof (safe intro!: exI[where x=\]) show "countable \" unfolding \_def by (intro countable_image countable_Collect_finite) fix A assume "A \ \" then show "x \ A" "open A" using \(4)[OF open_UNIV] by (auto simp: \_def intro: \ from_nat_into) next let ?int = "\N. \(from_nat_into \ ` N)" fix A B assume "A \ \" "B \ \" then obtain N M where "A = ?int N" "B = ?int M" "finite (N \ M)" by (auto simp: \_def) then show "A \ B \ \" by (auto simp: \_def intro!: image_eqI[where x="N \ M"]) next fix S assume "open S" "x \ S" then obtain a where a: "a\\" "a \ S" using \ by blast then show "\a\\. a \ S" using a \ by (intro bexI[where x=a]) (auto simp: \_def intro: image_eqI[where x="{to_nat_on \ a}"]) qed qed lemma (in topological_space) first_countableI: assumes "countable \" and 1: "\A. A \ \ \ x \ A" "\A. A \ \ \ open A" and 2: "\S. open S \ x \ S \ \A\\. A \ S" shows "\\::nat \ 'a set. (\i. x \ \ i \ open (\ i)) \ (\S. open S \ x \ S \ (\i. \ i \ S))" proof (safe intro!: exI[of _ "from_nat_into \"]) fix i have "\ \ {}" using 2[of UNIV] by auto show "x \ from_nat_into \ i" "open (from_nat_into \ i)" using range_from_nat_into_subset[OF \\ \ {}\] 1 by auto next fix S assume "open S" "x\S" from 2[OF this] show "\i. from_nat_into \ i \ S" using subset_range_from_nat_into[OF \countable \\] by auto qed instance prod :: (first_countable_topology, first_countable_topology) first_countable_topology proof fix x :: "'a \ 'b" obtain \ where \: "countable \" "\a. a \ \ \ fst x \ a" "\a. a \ \ \ open a" "\S. open S \ fst x \ S \ \a\\. a \ S" by (rule first_countable_basisE[of "fst x"]) blast obtain B where B: "countable B" "\a. a \ B \ snd x \ a" "\a. a \ B \ open a" "\S. open S \ snd x \ S \ \a\B. a \ S" by (rule first_countable_basisE[of "snd x"]) blast show "\\::nat \ ('a \ 'b) set. (\i. x \ \ i \ open (\ i)) \ (\S. open S \ x \ S \ (\i. \ i \ S))" proof (rule first_countableI[of "(\(a, b). a \ b) ` (\ \ B)"], safe) fix a b assume x: "a \ \" "b \ B" show "x \ a \ b" by (simp add: \(2) B(2) mem_Times_iff x) show "open (a \ b)" by (simp add: \(3) B(3) open_Times x) next fix S assume "open S" "x \ S" then obtain a' b' where a'b': "open a'" "open b'" "x \ a' \ b'" "a' \ b' \ S" by (rule open_prod_elim) moreover from a'b' \(4)[of a'] B(4)[of b'] obtain a b where "a \ \" "a \ a'" "b \ B" "b \ b'" by auto ultimately show "\a\(\(a, b). a \ b) ` (\ \ B). a \ S" by (auto intro!: bexI[of _ "a \ b"] bexI[of _ a] bexI[of _ b]) qed (simp add: \ B) qed class second_countable_topology = topological_space + assumes ex_countable_subbasis: "\B::'a set set. countable B \ open = generate_topology B" begin lemma ex_countable_basis: "\B::'a set set. countable B \ topological_basis B" proof - from ex_countable_subbasis obtain B where B: "countable B" "open = generate_topology B" by blast let ?B = "Inter ` {b. finite b \ b \ B }" show ?thesis proof (intro exI conjI) show "countable ?B" by (intro countable_image countable_Collect_finite_subset B) { fix S assume "open S" then have "\B'\{b. finite b \ b \ B}. (\b\B'. \b) = S" unfolding B proof induct case UNIV show ?case by (intro exI[of _ "{{}}"]) simp next case (Int a b) then obtain x y where x: "a = \(Inter ` x)" "\i. i \ x \ finite i \ i \ B" and y: "b = \(Inter ` y)" "\i. i \ y \ finite i \ i \ B" by blast show ?case unfolding x y Int_UN_distrib2 by (intro exI[of _ "{i \ j| i j. i \ x \ j \ y}"]) (auto dest: x(2) y(2)) next case (UN K) then have "\k\K. \B'\{b. finite b \ b \ B}. \ (Inter ` B') = k" by auto then obtain k where "\ka\K. k ka \ {b. finite b \ b \ B} \ \(Inter ` (k ka)) = ka" unfolding bchoice_iff .. then show "\B'\{b. finite b \ b \ B}. \ (Inter ` B') = \K" by (intro exI[of _ "\(k ` K)"]) auto next case (Basis S) then show ?case by (intro exI[of _ "{{S}}"]) auto qed then have "(\B'\Inter ` {b. finite b \ b \ B}. \B' = S)" unfolding subset_image_iff by blast } then show "topological_basis ?B" unfolding topological_basis_def by (safe intro!: open_Inter) (simp_all add: B generate_topology.Basis subset_eq) qed qed end lemma univ_second_countable: obtains \ :: "'a::second_countable_topology set set" where "countable \" "\C. C \ \ \ open C" "\S. open S \ \U. U \ \ \ S = \U" by (metis ex_countable_basis topological_basis_def) proposition Lindelof: fixes \ :: "'a::second_countable_topology set set" assumes \: "\S. S \ \ \ open S" obtains \' where "\' \ \" "countable \'" "\\' = \\" proof - obtain \ :: "'a set set" where "countable \" "\C. C \ \ \ open C" and \: "\S. open S \ \U. U \ \ \ S = \U" using univ_second_countable by blast define \ where "\ \ {S. S \ \ \ (\U. U \ \ \ S \ U)}" have "countable \" apply (rule countable_subset [OF _ \countable \\]) apply (force simp: \_def) done have "\S. \U. S \ \ \ U \ \ \ S \ U" by (simp add: \_def) then obtain G where G: "\S. S \ \ \ G S \ \ \ S \ G S" by metis have "\\ \ \\" unfolding \_def by (blast dest: \ \) moreover have "\\ \ \\" using \_def by blast ultimately have eq1: "\\ = \\" .. have eq2: "\\ = \ (G ` \)" using G eq1 by auto show ?thesis apply (rule_tac \' = "G ` \" in that) using G \countable \\ by (auto simp: eq1 eq2) qed lemma countable_disjoint_open_subsets: fixes \ :: "'a::second_countable_topology set set" assumes "\S. S \ \ \ open S" and pw: "pairwise disjnt \" shows "countable \" proof - obtain \' where "\' \ \" "countable \'" "\\' = \\" by (meson assms Lindelof) with pw have "\ \ insert {} \'" by (fastforce simp add: pairwise_def disjnt_iff) then show ?thesis by (simp add: \countable \'\ countable_subset) qed sublocale second_countable_topology < countable_basis "open" "SOME B. countable B \ topological_basis B" using someI_ex[OF ex_countable_basis] by unfold_locales safe instance prod :: (second_countable_topology, second_countable_topology) second_countable_topology proof obtain A :: "'a set set" where "countable A" "topological_basis A" using ex_countable_basis by auto moreover obtain B :: "'b set set" where "countable B" "topological_basis B" using ex_countable_basis by auto ultimately show "\B::('a \ 'b) set set. countable B \ open = generate_topology B" by (auto intro!: exI[of _ "(\(a, b). a \ b) ` (A \ B)"] topological_basis_prod topological_basis_imp_subbasis) qed instance second_countable_topology \ first_countable_topology proof fix x :: 'a define B :: "'a set set" where "B = (SOME B. countable B \ topological_basis B)" then have B: "countable B" "topological_basis B" using countable_basis is_basis by (auto simp: countable_basis is_basis) then show "\A::nat \ 'a set. (\i. x \ A i \ open (A i)) \ (\S. open S \ x \ S \ (\i. A i \ S))" by (intro first_countableI[of "{b\B. x \ b}"]) (fastforce simp: topological_space_class.topological_basis_def)+ qed instance nat :: second_countable_topology proof show "\B::nat set set. countable B \ open = generate_topology B" by (intro exI[of _ "range lessThan \ range greaterThan"]) (auto simp: open_nat_def) qed lemma countable_separating_set_linorder1: shows "\B::('a::{linorder_topology, second_countable_topology} set). countable B \ (\x y. x < y \ (\b \ B. x < b \ b \ y))" proof - obtain A::"'a set set" where "countable A" "topological_basis A" using ex_countable_basis by auto define B1 where "B1 = {(LEAST x. x \ U)| U. U \ A}" then have "countable B1" using \countable A\ by (simp add: Setcompr_eq_image) define B2 where "B2 = {(SOME x. x \ U)| U. U \ A}" then have "countable B2" using \countable A\ by (simp add: Setcompr_eq_image) have "\b \ B1 \ B2. x < b \ b \ y" if "x < y" for x y proof (cases) assume "\z. x < z \ z < y" then obtain z where z: "x < z \ z < y" by auto define U where "U = {x<.. U" using z U_def by simp ultimately obtain V where "V \ A" "z \ V" "V \ U" using topological_basisE[OF \topological_basis A\] by auto define w where "w = (SOME x. x \ V)" then have "w \ V" using \z \ V\ by (metis someI2) then have "x < w \ w \ y" using \w \ V\ \V \ U\ U_def by fastforce moreover have "w \ B1 \ B2" using w_def B2_def \V \ A\ by auto ultimately show ?thesis by auto next assume "\(\z. x < z \ z < y)" then have *: "\z. z > x \ z \ y" by auto define U where "U = {x<..}" then have "open U" by simp moreover have "y \ U" using \x < y\ U_def by simp ultimately obtain "V" where "V \ A" "y \ V" "V \ U" using topological_basisE[OF \topological_basis A\] by auto have "U = {y..}" unfolding U_def using * \x < y\ by auto then have "V \ {y..}" using \V \ U\ by simp then have "(LEAST w. w \ V) = y" using \y \ V\ by (meson Least_equality atLeast_iff subsetCE) then have "y \ B1 \ B2" using \V \ A\ B1_def by auto moreover have "x < y \ y \ y" using \x < y\ by simp ultimately show ?thesis by auto qed moreover have "countable (B1 \ B2)" using \countable B1\ \countable B2\ by simp ultimately show ?thesis by auto qed lemma countable_separating_set_linorder2: shows "\B::('a::{linorder_topology, second_countable_topology} set). countable B \ (\x y. x < y \ (\b \ B. x \ b \ b < y))" proof - obtain A::"'a set set" where "countable A" "topological_basis A" using ex_countable_basis by auto define B1 where "B1 = {(GREATEST x. x \ U) | U. U \ A}" then have "countable B1" using \countable A\ by (simp add: Setcompr_eq_image) define B2 where "B2 = {(SOME x. x \ U)| U. U \ A}" then have "countable B2" using \countable A\ by (simp add: Setcompr_eq_image) have "\b \ B1 \ B2. x \ b \ b < y" if "x < y" for x y proof (cases) assume "\z. x < z \ z < y" then obtain z where z: "x < z \ z < y" by auto define U where "U = {x<.. U" using z U_def by simp ultimately obtain "V" where "V \ A" "z \ V" "V \ U" using topological_basisE[OF \topological_basis A\] by auto define w where "w = (SOME x. x \ V)" then have "w \ V" using \z \ V\ by (metis someI2) then have "x \ w \ w < y" using \w \ V\ \V \ U\ U_def by fastforce moreover have "w \ B1 \ B2" using w_def B2_def \V \ A\ by auto ultimately show ?thesis by auto next assume "\(\z. x < z \ z < y)" then have *: "\z. z < y \ z \ x" using leI by blast define U where "U = {.. U" using \x < y\ U_def by simp ultimately obtain "V" where "V \ A" "x \ V" "V \ U" using topological_basisE[OF \topological_basis A\] by auto have "U = {..x}" unfolding U_def using * \x < y\ by auto then have "V \ {..x}" using \V \ U\ by simp then have "(GREATEST x. x \ V) = x" using \x \ V\ by (meson Greatest_equality atMost_iff subsetCE) then have "x \ B1 \ B2" using \V \ A\ B1_def by auto moreover have "x \ x \ x < y" using \x < y\ by simp ultimately show ?thesis by auto qed moreover have "countable (B1 \ B2)" using \countable B1\ \countable B2\ by simp ultimately show ?thesis by auto qed lemma countable_separating_set_dense_linorder: shows "\B::('a::{linorder_topology, dense_linorder, second_countable_topology} set). countable B \ (\x y. x < y \ (\b \ B. x < b \ b < y))" proof - obtain B::"'a set" where B: "countable B" "\x y. x < y \ (\b \ B. x < b \ b \ y)" using countable_separating_set_linorder1 by auto have "\b \ B. x < b \ b < y" if "x < y" for x y proof - obtain z where "x < z" "z < y" using \x < y\ dense by blast then obtain b where "b \ B" "x < b \ b \ z" using B(2) by auto then have "x < b \ b < y" using \z < y\ by auto then show ?thesis using \b \ B\ by auto qed then show ?thesis using B(1) by auto qed subsection \Polish spaces\ text \Textbooks define Polish spaces as completely metrizable. We assume the topology to be complete for a given metric.\ class polish_space = complete_space + second_countable_topology subsection \Limit Points\ definition\<^marker>\tag important\ (in topological_space) islimpt:: "'a \ 'a set \ bool" (infixr "islimpt" 60) where "x islimpt S \ (\T. x\T \ open T \ (\y\S. y\T \ y\x))" lemma islimptI: assumes "\T. x \ T \ open T \ \y\S. y \ T \ y \ x" shows "x islimpt S" using assms unfolding islimpt_def by auto lemma islimptE: assumes "x islimpt S" and "x \ T" and "open T" obtains y where "y \ S" and "y \ T" and "y \ x" using assms unfolding islimpt_def by auto lemma islimpt_iff_eventually: "x islimpt S \ \ eventually (\y. y \ S) (at x)" unfolding islimpt_def eventually_at_topological by auto lemma islimpt_subset: "x islimpt S \ S \ T \ x islimpt T" unfolding islimpt_def by fast lemma islimpt_UNIV_iff: "x islimpt UNIV \ \ open {x}" unfolding islimpt_def by (safe, fast, case_tac "T = {x}", fast, fast) lemma islimpt_punctured: "x islimpt S = x islimpt (S-{x})" unfolding islimpt_def by blast text \A perfect space has no isolated points.\ lemma islimpt_UNIV [simp, intro]: "x islimpt UNIV" for x :: "'a::perfect_space" unfolding islimpt_UNIV_iff by (rule not_open_singleton) lemma closed_limpt: "closed S \ (\x. x islimpt S \ x \ S)" unfolding closed_def apply (subst open_subopen) apply (simp add: islimpt_def subset_eq) apply (metis ComplE ComplI) done lemma islimpt_EMPTY[simp]: "\ x islimpt {}" by (auto simp: islimpt_def) lemma islimpt_Un: "x islimpt (S \ T) \ x islimpt S \ x islimpt T" by (simp add: islimpt_iff_eventually eventually_conj_iff) lemma islimpt_insert: fixes x :: "'a::t1_space" shows "x islimpt (insert a s) \ x islimpt s" proof assume *: "x islimpt (insert a s)" show "x islimpt s" proof (rule islimptI) fix t assume t: "x \ t" "open t" show "\y\s. y \ t \ y \ x" proof (cases "x = a") case True obtain y where "y \ insert a s" "y \ t" "y \ x" using * t by (rule islimptE) with \x = a\ show ?thesis by auto next case False with t have t': "x \ t - {a}" "open (t - {a})" by (simp_all add: open_Diff) obtain y where "y \ insert a s" "y \ t - {a}" "y \ x" using * t' by (rule islimptE) then show ?thesis by auto qed qed next assume "x islimpt s" then show "x islimpt (insert a s)" by (rule islimpt_subset) auto qed lemma islimpt_finite: fixes x :: "'a::t1_space" shows "finite s \ \ x islimpt s" by (induct set: finite) (simp_all add: islimpt_insert) lemma islimpt_Un_finite: fixes x :: "'a::t1_space" shows "finite s \ x islimpt (s \ t) \ x islimpt t" by (simp add: islimpt_Un islimpt_finite) lemma islimpt_eq_acc_point: fixes l :: "'a :: t1_space" shows "l islimpt S \ (\U. l\U \ open U \ infinite (U \ S))" proof (safe intro!: islimptI) fix U assume "l islimpt S" "l \ U" "open U" "finite (U \ S)" then have "l islimpt S" "l \ (U - (U \ S - {l}))" "open (U - (U \ S - {l}))" by (auto intro: finite_imp_closed) then show False by (rule islimptE) auto next fix T assume *: "\U. l\U \ open U \ infinite (U \ S)" "l \ T" "open T" then have "infinite (T \ S - {l})" by auto then have "\x. x \ (T \ S - {l})" unfolding ex_in_conv by (intro notI) simp then show "\y\S. y \ T \ y \ l" by auto qed lemma acc_point_range_imp_convergent_subsequence: fixes l :: "'a :: first_countable_topology" assumes l: "\U. l\U \ open U \ infinite (U \ range f)" shows "\r::nat\nat. strict_mono r \ (f \ r) \ l" proof - from countable_basis_at_decseq[of l] obtain A where A: "\i. open (A i)" "\i. l \ A i" "\S. open S \ l \ S \ eventually (\i. A i \ S) sequentially" by blast define s where "s n i = (SOME j. i < j \ f j \ A (Suc n))" for n i { fix n i have "infinite (A (Suc n) \ range f - f`{.. i})" using l A by auto then have "\x. x \ A (Suc n) \ range f - f`{.. i}" unfolding ex_in_conv by (intro notI) simp then have "\j. f j \ A (Suc n) \ j \ {.. i}" by auto then have "\a. i < a \ f a \ A (Suc n)" by (auto simp: not_le) then have "i < s n i" "f (s n i) \ A (Suc n)" unfolding s_def by (auto intro: someI2_ex) } note s = this define r where "r = rec_nat (s 0 0) s" have "strict_mono r" by (auto simp: r_def s strict_mono_Suc_iff) moreover have "(\n. f (r n)) \ l" proof (rule topological_tendstoI) fix S assume "open S" "l \ S" with A(3) have "eventually (\i. A i \ S) sequentially" by auto moreover { fix i assume "Suc 0 \ i" then have "f (r i) \ A i" by (cases i) (simp_all add: r_def s) } then have "eventually (\i. f (r i) \ A i) sequentially" by (auto simp: eventually_sequentially) ultimately show "eventually (\i. f (r i) \ S) sequentially" by eventually_elim auto qed ultimately show "\r::nat\nat. strict_mono r \ (f \ r) \ l" by (auto simp: convergent_def comp_def) qed lemma islimpt_range_imp_convergent_subsequence: fixes l :: "'a :: {t1_space, first_countable_topology}" assumes l: "l islimpt (range f)" shows "\r::nat\nat. strict_mono r \ (f \ r) \ l" using l unfolding islimpt_eq_acc_point by (rule acc_point_range_imp_convergent_subsequence) lemma sequence_unique_limpt: fixes f :: "nat \ 'a::t2_space" assumes "(f \ l) sequentially" and "l' islimpt (range f)" shows "l' = l" proof (rule ccontr) assume "l' \ l" obtain s t where "open s" "open t" "l' \ s" "l \ t" "s \ t = {}" using hausdorff [OF \l' \ l\] by auto have "eventually (\n. f n \ t) sequentially" using assms(1) \open t\ \l \ t\ by (rule topological_tendstoD) then obtain N where "\n\N. f n \ t" unfolding eventually_sequentially by auto have "UNIV = {.. {N..}" by auto then have "l' islimpt (f ` ({.. {N..}))" using assms(2) by simp then have "l' islimpt (f ` {.. f ` {N..})" by (simp add: image_Un) then have "l' islimpt (f ` {N..})" by (simp add: islimpt_Un_finite) then obtain y where "y \ f ` {N..}" "y \ s" "y \ l'" using \l' \ s\ \open s\ by (rule islimptE) then obtain n where "N \ n" "f n \ s" "f n \ l'" by auto with \\n\N. f n \ t\ have "f n \ s \ t" by simp with \s \ t = {}\ show False by simp qed subsection \Interior of a Set\ definition\<^marker>\tag important\ interior :: "('a::topological_space) set \ 'a set" where "interior S = \{T. open T \ T \ S}" lemma interiorI [intro?]: assumes "open T" and "x \ T" and "T \ S" shows "x \ interior S" using assms unfolding interior_def by fast lemma interiorE [elim?]: assumes "x \ interior S" obtains T where "open T" and "x \ T" and "T \ S" using assms unfolding interior_def by fast lemma open_interior [simp, intro]: "open (interior S)" by (simp add: interior_def open_Union) lemma interior_subset: "interior S \ S" by (auto simp: interior_def) lemma interior_maximal: "T \ S \ open T \ T \ interior S" by (auto simp: interior_def) lemma interior_open: "open S \ interior S = S" by (intro equalityI interior_subset interior_maximal subset_refl) lemma interior_eq: "interior S = S \ open S" by (metis open_interior interior_open) lemma open_subset_interior: "open S \ S \ interior T \ S \ T" by (metis interior_maximal interior_subset subset_trans) lemma interior_empty [simp]: "interior {} = {}" using open_empty by (rule interior_open) lemma interior_UNIV [simp]: "interior UNIV = UNIV" using open_UNIV by (rule interior_open) lemma interior_interior [simp]: "interior (interior S) = interior S" using open_interior by (rule interior_open) lemma interior_mono: "S \ T \ interior S \ interior T" by (auto simp: interior_def) lemma interior_unique: assumes "T \ S" and "open T" assumes "\T'. T' \ S \ open T' \ T' \ T" shows "interior S = T" by (intro equalityI assms interior_subset open_interior interior_maximal) lemma interior_singleton [simp]: "interior {a} = {}" for a :: "'a::perfect_space" - apply (rule interior_unique, simp_all) - using not_open_singleton subset_singletonD - apply fastforce - done + by (meson interior_eq interior_subset not_open_singleton subset_singletonD) lemma interior_Int [simp]: "interior (S \ T) = interior S \ interior T" - by (intro equalityI Int_mono Int_greatest interior_mono Int_lower1 - Int_lower2 interior_maximal interior_subset open_Int open_interior) + by (meson Int_mono Int_subset_iff antisym_conv interior_maximal interior_subset open_Int open_interior) lemma eventually_nhds_in_nhd: "x \ interior s \ eventually (\y. y \ s) (nhds x)" using interior_subset[of s] by (subst eventually_nhds) blast lemma interior_limit_point [intro]: fixes x :: "'a::perfect_space" assumes x: "x \ interior S" shows "x islimpt S" using x islimpt_UNIV [of x] unfolding interior_def islimpt_def apply (clarsimp, rename_tac T T') apply (drule_tac x="T \ T'" in spec) apply (auto simp: open_Int) done lemma interior_closed_Un_empty_interior: assumes cS: "closed S" and iT: "interior T = {}" shows "interior (S \ T) = interior S" proof show "interior S \ interior (S \ T)" by (rule interior_mono) (rule Un_upper1) show "interior (S \ T) \ interior S" proof fix x assume "x \ interior (S \ T)" then obtain R where "open R" "x \ R" "R \ S \ T" .. show "x \ interior S" proof (rule ccontr) assume "x \ interior S" with \x \ R\ \open R\ obtain y where "y \ R - S" unfolding interior_def by fast from \open R\ \closed S\ have "open (R - S)" by (rule open_Diff) from \R \ S \ T\ have "R - S \ T" by fast from \y \ R - S\ \open (R - S)\ \R - S \ T\ \interior T = {}\ show False unfolding interior_def by fast qed qed qed lemma interior_Times: "interior (A \ B) = interior A \ interior B" proof (rule interior_unique) show "interior A \ interior B \ A \ B" by (intro Sigma_mono interior_subset) show "open (interior A \ interior B)" by (intro open_Times open_interior) fix T assume "T \ A \ B" and "open T" then show "T \ interior A \ interior B" proof safe fix x y assume "(x, y) \ T" then obtain C D where "open C" "open D" "C \ D \ T" "x \ C" "y \ D" using \open T\ unfolding open_prod_def by fast then have "open C" "open D" "C \ A" "D \ B" "x \ C" "y \ D" using \T \ A \ B\ by auto then show "x \ interior A" and "y \ interior B" by (auto intro: interiorI) qed qed lemma interior_Ici: fixes x :: "'a :: {dense_linorder,linorder_topology}" assumes "b < x" shows "interior {x ..} = {x <..}" proof (rule interior_unique) fix T assume "T \ {x ..}" "open T" moreover have "x \ T" proof assume "x \ T" obtain y where "y < x" "{y <.. x} \ T" using open_left[OF \open T\ \x \ T\ \b < x\] by auto with dense[OF \y < x\] obtain z where "z \ T" "z < x" by (auto simp: subset_eq Ball_def) with \T \ {x ..}\ show False by auto qed ultimately show "T \ {x <..}" by (auto simp: subset_eq less_le) qed auto lemma interior_Iic: fixes x :: "'a ::{dense_linorder,linorder_topology}" assumes "x < b" shows "interior {.. x} = {..< x}" proof (rule interior_unique) fix T assume "T \ {.. x}" "open T" moreover have "x \ T" proof assume "x \ T" obtain y where "x < y" "{x ..< y} \ T" using open_right[OF \open T\ \x \ T\ \x < b\] by auto with dense[OF \x < y\] obtain z where "z \ T" "x < z" by (auto simp: subset_eq Ball_def less_le) with \T \ {.. x}\ show False by auto qed ultimately show "T \ {..< x}" by (auto simp: subset_eq less_le) qed auto lemma countable_disjoint_nonempty_interior_subsets: fixes \ :: "'a::second_countable_topology set set" assumes pw: "pairwise disjnt \" and int: "\S. \S \ \; interior S = {}\ \ S = {}" shows "countable \" proof (rule countable_image_inj_on) have "disjoint (interior ` \)" using pw by (simp add: disjoint_image_subset interior_subset) then show "countable (interior ` \)" by (auto intro: countable_disjoint_open_subsets) show "inj_on interior \" using pw apply (clarsimp simp: inj_on_def pairwise_def) apply (metis disjnt_def disjnt_subset1 inf.orderE int interior_subset) done qed subsection \Closure of a Set\ definition\<^marker>\tag important\ closure :: "('a::topological_space) set \ 'a set" where "closure S = S \ {x . x islimpt S}" lemma interior_closure: "interior S = - (closure (- S))" by (auto simp: interior_def closure_def islimpt_def) lemma closure_interior: "closure S = - interior (- S)" by (simp add: interior_closure) lemma closed_closure[simp, intro]: "closed (closure S)" by (simp add: closure_interior closed_Compl) lemma closure_subset: "S \ closure S" by (simp add: closure_def) lemma closure_hull: "closure S = closed hull S" by (auto simp: hull_def closure_interior interior_def) lemma closure_eq: "closure S = S \ closed S" unfolding closure_hull using closed_Inter by (rule hull_eq) lemma closure_closed [simp]: "closed S \ closure S = S" by (simp only: closure_eq) lemma closure_closure [simp]: "closure (closure S) = closure S" unfolding closure_hull by (rule hull_hull) lemma closure_mono: "S \ T \ closure S \ closure T" unfolding closure_hull by (rule hull_mono) lemma closure_minimal: "S \ T \ closed T \ closure S \ T" unfolding closure_hull by (rule hull_minimal) lemma closure_unique: assumes "S \ T" and "closed T" and "\T'. S \ T' \ closed T' \ T \ T'" shows "closure S = T" using assms unfolding closure_hull by (rule hull_unique) lemma closure_empty [simp]: "closure {} = {}" using closed_empty by (rule closure_closed) lemma closure_UNIV [simp]: "closure UNIV = UNIV" using closed_UNIV by (rule closure_closed) lemma closure_Un [simp]: "closure (S \ T) = closure S \ closure T" by (simp add: closure_interior) lemma closure_eq_empty [iff]: "closure S = {} \ S = {}" using closure_empty closure_subset[of S] by blast lemma closure_subset_eq: "closure S \ S \ closed S" using closure_eq[of S] closure_subset[of S] by simp lemma open_Int_closure_eq_empty: "open S \ (S \ closure T) = {} \ S \ T = {}" using open_subset_interior[of S "- T"] using interior_subset[of "- T"] by (auto simp: closure_interior) lemma open_Int_closure_subset: "open S \ S \ closure T \ closure (S \ T)" proof fix x assume *: "open S" "x \ S \ closure T" have "x islimpt (S \ T)" if **: "x islimpt T" proof (rule islimptI) fix A assume "x \ A" "open A" with * have "x \ A \ S" "open (A \ S)" by (simp_all add: open_Int) with ** obtain y where "y \ T" "y \ A \ S" "y \ x" by (rule islimptE) then have "y \ S \ T" "y \ A \ y \ x" by simp_all then show "\y\(S \ T). y \ A \ y \ x" .. qed with * show "x \ closure (S \ T)" unfolding closure_def by blast qed lemma closure_complement: "closure (- S) = - interior S" by (simp add: closure_interior) lemma interior_complement: "interior (- S) = - closure S" by (simp add: closure_interior) lemma interior_diff: "interior(S - T) = interior S - closure T" by (simp add: Diff_eq interior_complement) lemma closure_Times: "closure (A \ B) = closure A \ closure B" proof (rule closure_unique) show "A \ B \ closure A \ closure B" by (intro Sigma_mono closure_subset) show "closed (closure A \ closure B)" by (intro closed_Times closed_closure) fix T assume "A \ B \ T" and "closed T" then show "closure A \ closure B \ T" apply (simp add: closed_def open_prod_def, clarify) apply (rule ccontr) apply (drule_tac x="(a, b)" in bspec, simp, clarify, rename_tac C D) apply (simp add: closure_interior interior_def) apply (drule_tac x=C in spec) apply (drule_tac x=D in spec, auto) done qed lemma closure_open_Int_superset: assumes "open S" "S \ closure T" shows "closure(S \ T) = closure S" proof - have "closure S \ closure(S \ T)" by (metis assms closed_closure closure_minimal inf.orderE open_Int_closure_subset) then show ?thesis by (simp add: closure_mono dual_order.antisym) qed lemma closure_Int: "closure (\I) \ \{closure S |S. S \ I}" proof - { fix y assume "y \ \I" then have y: "\S \ I. y \ S" by auto { fix S assume "S \ I" then have "y \ closure S" using closure_subset y by auto } then have "y \ \{closure S |S. S \ I}" by auto } then have "\I \ \{closure S |S. S \ I}" by auto moreover have "closed (\{closure S |S. S \ I})" unfolding closed_Inter closed_closure by auto ultimately show ?thesis using closure_hull[of "\I"] hull_minimal[of "\I" "\{closure S |S. S \ I}" "closed"] by auto qed lemma islimpt_in_closure: "(x islimpt S) = (x\closure(S-{x}))" unfolding closure_def using islimpt_punctured by blast lemma connected_imp_connected_closure: "connected S \ connected (closure S)" by (rule connectedI) (meson closure_subset open_Int open_Int_closure_eq_empty subset_trans connectedD) lemma bdd_below_closure: fixes A :: "real set" assumes "bdd_below A" shows "bdd_below (closure A)" proof - from assms obtain m where "\x. x \ A \ m \ x" by (auto simp: bdd_below_def) then have "A \ {m..}" by auto then have "closure A \ {m..}" using closed_real_atLeast by (rule closure_minimal) then show ?thesis by (auto simp: bdd_below_def) qed subsection \Frontier (also known as boundary)\ definition\<^marker>\tag important\ frontier :: "('a::topological_space) set \ 'a set" where "frontier S = closure S - interior S" lemma frontier_closed [iff]: "closed (frontier S)" by (simp add: frontier_def closed_Diff) lemma frontier_closures: "frontier S = closure S \ closure (- S)" by (auto simp: frontier_def interior_closure) lemma frontier_Int: "frontier(S \ T) = closure(S \ T) \ (frontier S \ frontier T)" proof - have "closure (S \ T) \ closure S" "closure (S \ T) \ closure T" by (simp_all add: closure_mono) then show ?thesis by (auto simp: frontier_closures) qed lemma frontier_Int_subset: "frontier(S \ T) \ frontier S \ frontier T" by (auto simp: frontier_Int) lemma frontier_Int_closed: assumes "closed S" "closed T" shows "frontier(S \ T) = (frontier S \ T) \ (S \ frontier T)" proof - have "closure (S \ T) = T \ S" using assms by (simp add: Int_commute closed_Int) moreover have "T \ (closure S \ closure (- S)) = frontier S \ T" by (simp add: Int_commute frontier_closures) ultimately show ?thesis by (simp add: Int_Un_distrib Int_assoc Int_left_commute assms frontier_closures) qed lemma frontier_subset_closed: "closed S \ frontier S \ S" by (metis frontier_def closure_closed Diff_subset) lemma frontier_empty [simp]: "frontier {} = {}" by (simp add: frontier_def) lemma frontier_subset_eq: "frontier S \ S \ closed S" proof - { assume "frontier S \ S" then have "closure S \ S" using interior_subset unfolding frontier_def by auto then have "closed S" using closure_subset_eq by auto } then show ?thesis using frontier_subset_closed[of S] .. qed lemma frontier_complement [simp]: "frontier (- S) = frontier S" by (auto simp: frontier_def closure_complement interior_complement) lemma frontier_Un_subset: "frontier(S \ T) \ frontier S \ frontier T" by (metis compl_sup frontier_Int_subset frontier_complement) lemma frontier_disjoint_eq: "frontier S \ S = {} \ open S" using frontier_complement frontier_subset_eq[of "- S"] unfolding open_closed by auto lemma frontier_UNIV [simp]: "frontier UNIV = {}" using frontier_complement frontier_empty by fastforce lemma frontier_interiors: "frontier s = - interior(s) - interior(-s)" by (simp add: Int_commute frontier_def interior_closure) lemma frontier_interior_subset: "frontier(interior S) \ frontier S" by (simp add: Diff_mono frontier_interiors interior_mono interior_subset) lemma closure_Un_frontier: "closure S = S \ frontier S" proof - have "S \ interior S = S" using interior_subset by auto then show ?thesis using closure_subset by (auto simp: frontier_def) qed subsection\<^marker>\tag unimportant\ \Filters and the ``eventually true'' quantifier\ text \Identify Trivial limits, where we can't approach arbitrarily closely.\ lemma trivial_limit_within: "trivial_limit (at a within S) \ \ a islimpt S" proof assume "trivial_limit (at a within S)" then show "\ a islimpt S" unfolding trivial_limit_def unfolding eventually_at_topological unfolding islimpt_def apply (clarsimp simp add: set_eq_iff) apply (rename_tac T, rule_tac x=T in exI) apply (clarsimp, drule_tac x=y in bspec, simp_all) done next assume "\ a islimpt S" then show "trivial_limit (at a within S)" unfolding trivial_limit_def eventually_at_topological islimpt_def by metis qed lemma trivial_limit_at_iff: "trivial_limit (at a) \ \ a islimpt UNIV" using trivial_limit_within [of a UNIV] by simp lemma trivial_limit_at: "\ trivial_limit (at a)" for a :: "'a::perfect_space" by (rule at_neq_bot) lemma not_trivial_limit_within: "\ trivial_limit (at x within S) = (x \ closure (S - {x}))" using islimpt_in_closure by (metis trivial_limit_within) lemma not_in_closure_trivial_limitI: "x \ closure s \ trivial_limit (at x within s)" using not_trivial_limit_within[of x s] by safe (metis Diff_empty Diff_insert0 closure_subset contra_subsetD) lemma filterlim_at_within_closure_implies_filterlim: "filterlim f l (at x within s)" if "x \ closure s \ filterlim f l (at x within s)" by (metis bot.extremum filterlim_filtercomap filterlim_mono not_in_closure_trivial_limitI that) lemma at_within_eq_bot_iff: "at c within A = bot \ c \ closure (A - {c})" using not_trivial_limit_within[of c A] by blast text \Some property holds "sufficiently close" to the limit point.\ lemma trivial_limit_eventually: "trivial_limit net \ eventually P net" by simp lemma trivial_limit_eq: "trivial_limit net \ (\P. eventually P net)" by (simp add: filter_eq_iff) lemma Lim_topological: "(f \ l) net \ trivial_limit net \ (\S. open S \ l \ S \ eventually (\x. f x \ S) net)" unfolding tendsto_def trivial_limit_eq by auto lemma eventually_within_Un: "eventually P (at x within (s \ t)) \ eventually P (at x within s) \ eventually P (at x within t)" unfolding eventually_at_filter by (auto elim!: eventually_rev_mp) lemma Lim_within_union: "(f \ l) (at x within (s \ t)) \ (f \ l) (at x within s) \ (f \ l) (at x within t)" unfolding tendsto_def by (auto simp: eventually_within_Un) subsection \Limits\ text \The expected monotonicity property.\ lemma Lim_Un: assumes "(f \ l) (at x within S)" "(f \ l) (at x within T)" shows "(f \ l) (at x within (S \ T))" using assms unfolding at_within_union by (rule filterlim_sup) lemma Lim_Un_univ: "(f \ l) (at x within S) \ (f \ l) (at x within T) \ S \ T = UNIV \ (f \ l) (at x)" by (metis Lim_Un) text \Interrelations between restricted and unrestricted limits.\ lemma Lim_at_imp_Lim_at_within: "(f \ l) (at x) \ (f \ l) (at x within S)" by (metis order_refl filterlim_mono subset_UNIV at_le) lemma eventually_within_interior: assumes "x \ interior S" shows "eventually P (at x within S) \ eventually P (at x)" (is "?lhs = ?rhs") proof from assms obtain T where T: "open T" "x \ T" "T \ S" .. { assume ?lhs then obtain A where "open A" and "x \ A" and "\y\A. y \ x \ y \ S \ P y" by (auto simp: eventually_at_topological) with T have "open (A \ T)" and "x \ A \ T" and "\y \ A \ T. y \ x \ P y" by auto then show ?rhs by (auto simp: eventually_at_topological) next assume ?rhs then show ?lhs by (auto elim: eventually_mono simp: eventually_at_filter) } qed lemma at_within_interior: "x \ interior S \ at x within S = at x" unfolding filter_eq_iff by (intro allI eventually_within_interior) lemma Lim_within_LIMSEQ: fixes a :: "'a::first_countable_topology" assumes "\S. (\n. S n \ a \ S n \ T) \ S \ a \ (\n. X (S n)) \ L" shows "(X \ L) (at a within T)" using assms unfolding tendsto_def [where l=L] by (simp add: sequentially_imp_eventually_within) lemma Lim_right_bound: fixes f :: "'a :: {linorder_topology, conditionally_complete_linorder, no_top} \ 'b::{linorder_topology, conditionally_complete_linorder}" assumes mono: "\a b. a \ I \ b \ I \ x < a \ a \ b \ f a \ f b" and bnd: "\a. a \ I \ x < a \ K \ f a" shows "(f \ Inf (f ` ({x<..} \ I))) (at x within ({x<..} \ I))" proof (cases "{x<..} \ I = {}") case True then show ?thesis by simp next case False show ?thesis proof (rule order_tendstoI) fix a assume a: "a < Inf (f ` ({x<..} \ I))" { fix y assume "y \ {x<..} \ I" with False bnd have "Inf (f ` ({x<..} \ I)) \ f y" by (auto intro!: cInf_lower bdd_belowI2) with a have "a < f y" by (blast intro: less_le_trans) } then show "eventually (\x. a < f x) (at x within ({x<..} \ I))" by (auto simp: eventually_at_filter intro: exI[of _ 1] zero_less_one) next fix a assume "Inf (f ` ({x<..} \ I)) < a" from cInf_lessD[OF _ this] False obtain y where y: "x < y" "y \ I" "f y < a" by auto then have "eventually (\x. x \ I \ f x < a) (at_right x)" unfolding eventually_at_right[OF \x < y\] by (metis less_imp_le le_less_trans mono) then show "eventually (\x. f x < a) (at x within ({x<..} \ I))" unfolding eventually_at_filter by eventually_elim simp qed qed (*could prove directly from islimpt_sequential_inj, but only for metric spaces*) lemma islimpt_sequential: fixes x :: "'a::first_countable_topology" shows "x islimpt S \ (\f. (\n::nat. f n \ S - {x}) \ (f \ x) sequentially)" (is "?lhs = ?rhs") proof assume ?lhs from countable_basis_at_decseq[of x] obtain A where A: "\i. open (A i)" "\i. x \ A i" "\S. open S \ x \ S \ eventually (\i. A i \ S) sequentially" by blast define f where "f n = (SOME y. y \ S \ y \ A n \ x \ y)" for n { fix n from \?lhs\ have "\y. y \ S \ y \ A n \ x \ y" unfolding islimpt_def using A(1,2)[of n] by auto then have "f n \ S \ f n \ A n \ x \ f n" unfolding f_def by (rule someI_ex) then have "f n \ S" "f n \ A n" "x \ f n" by auto } then have "\n. f n \ S - {x}" by auto moreover have "(\n. f n) \ x" proof (rule topological_tendstoI) fix S assume "open S" "x \ S" from A(3)[OF this] \\n. f n \ A n\ show "eventually (\x. f x \ S) sequentially" by (auto elim!: eventually_mono) qed ultimately show ?rhs by fast next assume ?rhs then obtain f :: "nat \ 'a" where f: "\n. f n \ S - {x}" and lim: "f \ x" by auto show ?lhs unfolding islimpt_def proof safe fix T assume "open T" "x \ T" from lim[THEN topological_tendstoD, OF this] f show "\y\S. y \ T \ y \ x" unfolding eventually_sequentially by auto qed qed text\These are special for limits out of the same topological space.\ lemma Lim_within_id: "(id \ a) (at a within s)" unfolding id_def by (rule tendsto_ident_at) lemma Lim_at_id: "(id \ a) (at a)" unfolding id_def by (rule tendsto_ident_at) text\It's also sometimes useful to extract the limit point from the filter.\ abbreviation netlimit :: "'a::t2_space filter \ 'a" where "netlimit F \ Lim F (\x. x)" lemma netlimit_at [simp]: fixes a :: "'a::{perfect_space,t2_space}" shows "netlimit (at a) = a" using Lim_ident_at [of a UNIV] by simp lemma lim_within_interior: "x \ interior S \ (f \ l) (at x within S) \ (f \ l) (at x)" by (metis at_within_interior) lemma netlimit_within_interior: fixes x :: "'a::{t2_space,perfect_space}" assumes "x \ interior S" shows "netlimit (at x within S) = x" using assms by (metis at_within_interior netlimit_at) text\Useful lemmas on closure and set of possible sequential limits.\ lemma closure_sequential: fixes l :: "'a::first_countable_topology" shows "l \ closure S \ (\x. (\n. x n \ S) \ (x \ l) sequentially)" (is "?lhs = ?rhs") proof assume "?lhs" moreover { assume "l \ S" then have "?rhs" using tendsto_const[of l sequentially] by auto } moreover { assume "l islimpt S" then have "?rhs" unfolding islimpt_sequential by auto } ultimately show "?rhs" unfolding closure_def by auto next assume "?rhs" then show "?lhs" unfolding closure_def islimpt_sequential by auto qed lemma closed_sequential_limits: fixes S :: "'a::first_countable_topology set" shows "closed S \ (\x l. (\n. x n \ S) \ (x \ l) sequentially \ l \ S)" by (metis closure_sequential closure_subset_eq subset_iff) lemma tendsto_If_within_closures: assumes f: "x \ s \ (closure s \ closure t) \ (f \ l x) (at x within s \ (closure s \ closure t))" assumes g: "x \ t \ (closure s \ closure t) \ (g \ l x) (at x within t \ (closure s \ closure t))" assumes "x \ s \ t" shows "((\x. if x \ s then f x else g x) \ l x) (at x within s \ t)" proof - have *: "(s \ t) \ {x. x \ s} = s" "(s \ t) \ {x. x \ s} = t - s" by auto have "(f \ l x) (at x within s)" by (rule filterlim_at_within_closure_implies_filterlim) (use \x \ _\ in \auto simp: inf_commute closure_def intro: tendsto_within_subset[OF f]\) moreover have "(g \ l x) (at x within t - s)" by (rule filterlim_at_within_closure_implies_filterlim) (use \x \ _\ in \auto intro!: tendsto_within_subset[OF g] simp: closure_def intro: islimpt_subset\) ultimately show ?thesis by (intro filterlim_at_within_If) (simp_all only: *) qed subsection \Compactness\ lemma brouwer_compactness_lemma: fixes f :: "'a::topological_space \ 'b::real_normed_vector" assumes "compact s" and "continuous_on s f" and "\ (\x\s. f x = 0)" obtains d where "0 < d" and "\x\s. d \ norm (f x)" proof (cases "s = {}") case True show thesis by (rule that [of 1]) (auto simp: True) next case False have "continuous_on s (norm \ f)" by (rule continuous_intros continuous_on_norm assms(2))+ with False obtain x where x: "x \ s" "\y\s. (norm \ f) x \ (norm \ f) y" using continuous_attains_inf[OF assms(1), of "norm \ f"] unfolding o_def by auto have "(norm \ f) x > 0" using assms(3) and x(1) by auto then show ?thesis by (rule that) (insert x(2), auto simp: o_def) qed subsubsection \Bolzano-Weierstrass property\ proposition Heine_Borel_imp_Bolzano_Weierstrass: assumes "compact s" and "infinite t" and "t \ s" shows "\x \ s. x islimpt t" proof (rule ccontr) assume "\ (\x \ s. x islimpt t)" then obtain f where f: "\x\s. x \ f x \ open (f x) \ (\y\t. y \ f x \ y = x)" unfolding islimpt_def using bchoice[of s "\ x T. x \ T \ open T \ (\y\t. y \ T \ y = x)"] by auto obtain g where g: "g \ {t. \x. x \ s \ t = f x}" "finite g" "s \ \g" using assms(1)[unfolded compact_eq_Heine_Borel, THEN spec[where x="{t. \x. x\s \ t = f x}"]] using f by auto from g(1,3) have g':"\x\g. \xa \ s. x = f xa" by auto { fix x y assume "x \ t" "y \ t" "f x = f y" then have "x \ f x" "y \ f x \ y = x" using f[THEN bspec[where x=x]] and \t \ s\ by auto then have "x = y" using \f x = f y\ and f[THEN bspec[where x=y]] and \y \ t\ and \t \ s\ by auto } then have "inj_on f t" unfolding inj_on_def by simp then have "infinite (f ` t)" using assms(2) using finite_imageD by auto moreover { fix x assume "x \ t" "f x \ g" from g(3) assms(3) \x \ t\ obtain h where "h \ g" and "x \ h" by auto then obtain y where "y \ s" "h = f y" using g'[THEN bspec[where x=h]] by auto then have "y = x" using f[THEN bspec[where x=y]] and \x\t\ and \x\h\[unfolded \h = f y\] by auto then have False using \f x \ g\ \h \ g\ unfolding \h = f y\ by auto } then have "f ` t \ g" by auto ultimately show False using g(2) using finite_subset by auto qed lemma sequence_infinite_lemma: fixes f :: "nat \ 'a::t1_space" assumes "\n. f n \ l" and "(f \ l) sequentially" shows "infinite (range f)" proof assume "finite (range f)" then have "closed (range f)" by (rule finite_imp_closed) then have "open (- range f)" by (rule open_Compl) from assms(1) have "l \ - range f" by auto from assms(2) have "eventually (\n. f n \ - range f) sequentially" using \open (- range f)\ \l \ - range f\ by (rule topological_tendstoD) then show False unfolding eventually_sequentially by auto qed lemma Bolzano_Weierstrass_imp_closed: fixes s :: "'a::{first_countable_topology,t2_space} set" assumes "\t. infinite t \ t \ s --> (\x \ s. x islimpt t)" shows "closed s" proof - { fix x l assume as: "\n::nat. x n \ s" "(x \ l) sequentially" then have "l \ s" proof (cases "\n. x n \ l") case False then show "l\s" using as(1) by auto next case True note cas = this with as(2) have "infinite (range x)" using sequence_infinite_lemma[of x l] by auto then obtain l' where "l'\s" "l' islimpt (range x)" using assms[THEN spec[where x="range x"]] as(1) by auto then show "l\s" using sequence_unique_limpt[of x l l'] using as cas by auto qed } then show ?thesis unfolding closed_sequential_limits by fast qed lemma closure_insert: fixes x :: "'a::t1_space" shows "closure (insert x s) = insert x (closure s)" apply (rule closure_unique) apply (rule insert_mono [OF closure_subset]) apply (rule closed_insert [OF closed_closure]) apply (simp add: closure_minimal) done text\In particular, some common special cases.\ lemma compact_Un [intro]: assumes "compact s" and "compact t" shows " compact (s \ t)" proof (rule compactI) fix f assume *: "Ball f open" "s \ t \ \f" from * \compact s\ obtain s' where "s' \ f \ finite s' \ s \ \s'" unfolding compact_eq_Heine_Borel by (auto elim!: allE[of _ f]) moreover from * \compact t\ obtain t' where "t' \ f \ finite t' \ t \ \t'" unfolding compact_eq_Heine_Borel by (auto elim!: allE[of _ f]) ultimately show "\f'\f. finite f' \ s \ t \ \f'" by (auto intro!: exI[of _ "s' \ t'"]) qed lemma compact_Union [intro]: "finite S \ (\T. T \ S \ compact T) \ compact (\S)" by (induct set: finite) auto lemma compact_UN [intro]: "finite A \ (\x. x \ A \ compact (B x)) \ compact (\x\A. B x)" by (rule compact_Union) auto lemma closed_Int_compact [intro]: assumes "closed s" and "compact t" shows "compact (s \ t)" using compact_Int_closed [of t s] assms by (simp add: Int_commute) lemma compact_Int [intro]: fixes s t :: "'a :: t2_space set" assumes "compact s" and "compact t" shows "compact (s \ t)" using assms by (intro compact_Int_closed compact_imp_closed) lemma compact_sing [simp]: "compact {a}" unfolding compact_eq_Heine_Borel by auto lemma compact_insert [simp]: assumes "compact s" shows "compact (insert x s)" proof - have "compact ({x} \ s)" using compact_sing assms by (rule compact_Un) then show ?thesis by simp qed lemma finite_imp_compact: "finite s \ compact s" by (induct set: finite) simp_all lemma open_delete: fixes s :: "'a::t1_space set" shows "open s \ open (s - {x})" by (simp add: open_Diff) text\Compactness expressed with filters\ lemma closure_iff_nhds_not_empty: "x \ closure X \ (\A. \S\A. open S \ x \ S \ X \ A \ {})" proof safe assume x: "x \ closure X" fix S A assume "open S" "x \ S" "X \ A = {}" "S \ A" then have "x \ closure (-S)" by (auto simp: closure_complement subset_eq[symmetric] intro: interiorI) with x have "x \ closure X - closure (-S)" by auto also have "\ \ closure (X \ S)" using \open S\ open_Int_closure_subset[of S X] by (simp add: closed_Compl ac_simps) finally have "X \ S \ {}" by auto then show False using \X \ A = {}\ \S \ A\ by auto next assume "\A S. S \ A \ open S \ x \ S \ X \ A \ {}" from this[THEN spec, of "- X", THEN spec, of "- closure X"] show "x \ closure X" by (simp add: closure_subset open_Compl) qed lemma compact_filter: "compact U \ (\F. F \ bot \ eventually (\x. x \ U) F \ (\x\U. inf (nhds x) F \ bot))" proof (intro allI iffI impI compact_fip[THEN iffD2] notI) fix F assume "compact U" assume F: "F \ bot" "eventually (\x. x \ U) F" then have "U \ {}" by (auto simp: eventually_False) define Z where "Z = closure ` {A. eventually (\x. x \ A) F}" then have "\z\Z. closed z" by auto moreover have ev_Z: "\z. z \ Z \ eventually (\x. x \ z) F" unfolding Z_def by (auto elim: eventually_mono intro: subsetD[OF closure_subset]) have "(\B \ Z. finite B \ U \ \B \ {})" proof (intro allI impI) fix B assume "finite B" "B \ Z" with \finite B\ ev_Z F(2) have "eventually (\x. x \ U \ (\B)) F" by (auto simp: eventually_ball_finite_distrib eventually_conj_iff) with F show "U \ \B \ {}" by (intro notI) (simp add: eventually_False) qed ultimately have "U \ \Z \ {}" using \compact U\ unfolding compact_fip by blast then obtain x where "x \ U" and x: "\z. z \ Z \ x \ z" by auto have "\P. eventually P (inf (nhds x) F) \ P \ bot" unfolding eventually_inf eventually_nhds proof safe fix P Q R S assume "eventually R F" "open S" "x \ S" with open_Int_closure_eq_empty[of S "{x. R x}"] x[of "closure {x. R x}"] have "S \ {x. R x} \ {}" by (auto simp: Z_def) moreover assume "Ball S Q" "\x. Q x \ R x \ bot x" ultimately show False by (auto simp: set_eq_iff) qed with \x \ U\ show "\x\U. inf (nhds x) F \ bot" by (metis eventually_bot) next fix A assume A: "\a\A. closed a" "\B\A. finite B \ U \ \B \ {}" "U \ \A = {}" define F where "F = (INF a\insert U A. principal a)" have "F \ bot" unfolding F_def proof (rule INF_filter_not_bot) fix X assume X: "X \ insert U A" "finite X" with A(2)[THEN spec, of "X - {U}"] have "U \ \(X - {U}) \ {}" by auto with X show "(INF a\X. principal a) \ bot" by (auto simp: INF_principal_finite principal_eq_bot_iff) qed moreover have "F \ principal U" unfolding F_def by auto then have "eventually (\x. x \ U) F" by (auto simp: le_filter_def eventually_principal) moreover assume "\F. F \ bot \ eventually (\x. x \ U) F \ (\x\U. inf (nhds x) F \ bot)" ultimately obtain x where "x \ U" and x: "inf (nhds x) F \ bot" by auto { fix V assume "V \ A" then have "F \ principal V" unfolding F_def by (intro INF_lower2[of V]) auto then have V: "eventually (\x. x \ V) F" by (auto simp: le_filter_def eventually_principal) have "x \ closure V" unfolding closure_iff_nhds_not_empty proof (intro impI allI) fix S A assume "open S" "x \ S" "S \ A" then have "eventually (\x. x \ A) (nhds x)" by (auto simp: eventually_nhds) with V have "eventually (\x. x \ V \ A) (inf (nhds x) F)" by (auto simp: eventually_inf) with x show "V \ A \ {}" by (auto simp del: Int_iff simp add: trivial_limit_def) qed then have "x \ V" using \V \ A\ A(1) by simp } with \x\U\ have "x \ U \ \A" by auto with \U \ \A = {}\ show False by auto qed definition\<^marker>\tag important\ countably_compact :: "('a::topological_space) set \ bool" where "countably_compact U \ (\A. countable A \ (\a\A. open a) \ U \ \A \ (\T\A. finite T \ U \ \T))" lemma countably_compactE: assumes "countably_compact s" and "\t\C. open t" and "s \ \C" "countable C" obtains C' where "C' \ C" and "finite C'" and "s \ \C'" using assms unfolding countably_compact_def by metis lemma countably_compactI: assumes "\C. \t\C. open t \ s \ \C \ countable C \ (\C'\C. finite C' \ s \ \C')" shows "countably_compact s" using assms unfolding countably_compact_def by metis lemma compact_imp_countably_compact: "compact U \ countably_compact U" by (auto simp: compact_eq_Heine_Borel countably_compact_def) lemma countably_compact_imp_compact: assumes "countably_compact U" and ccover: "countable B" "\b\B. open b" and basis: "\T x. open T \ x \ T \ x \ U \ \b\B. x \ b \ b \ U \ T" shows "compact U" using \countably_compact U\ unfolding compact_eq_Heine_Borel countably_compact_def proof safe fix A assume A: "\a\A. open a" "U \ \A" assume *: "\A. countable A \ (\a\A. open a) \ U \ \A \ (\T\A. finite T \ U \ \T)" moreover define C where "C = {b\B. \a\A. b \ U \ a}" ultimately have "countable C" "\a\C. open a" unfolding C_def using ccover by auto moreover have "\A \ U \ \C" proof safe fix x a assume "x \ U" "x \ a" "a \ A" with basis[of a x] A obtain b where "b \ B" "x \ b" "b \ U \ a" by blast with \a \ A\ show "x \ \C" unfolding C_def by auto qed then have "U \ \C" using \U \ \A\ by auto ultimately obtain T where T: "T\C" "finite T" "U \ \T" using * by metis then have "\t\T. \a\A. t \ U \ a" by (auto simp: C_def) then obtain f where "\t\T. f t \ A \ t \ U \ f t" unfolding bchoice_iff Bex_def .. with T show "\T\A. finite T \ U \ \T" unfolding C_def by (intro exI[of _ "f`T"]) fastforce qed proposition countably_compact_imp_compact_second_countable: "countably_compact U \ compact (U :: 'a :: second_countable_topology set)" proof (rule countably_compact_imp_compact) fix T and x :: 'a assume "open T" "x \ T" from topological_basisE[OF is_basis this] obtain b where "b \ (SOME B. countable B \ topological_basis B)" "x \ b" "b \ T" . then show "\b\SOME B. countable B \ topological_basis B. x \ b \ b \ U \ T" by blast qed (insert countable_basis topological_basis_open[OF is_basis], auto) lemma countably_compact_eq_compact: "countably_compact U \ compact (U :: 'a :: second_countable_topology set)" using countably_compact_imp_compact_second_countable compact_imp_countably_compact by blast subsubsection\Sequential compactness\ definition\<^marker>\tag important\ seq_compact :: "'a::topological_space set \ bool" where "seq_compact S \ (\f. (\n. f n \ S) \ (\l\S. \r::nat\nat. strict_mono r \ ((f \ r) \ l) sequentially))" lemma seq_compactI: assumes "\f. \n. f n \ S \ \l\S. \r::nat\nat. strict_mono r \ ((f \ r) \ l) sequentially" shows "seq_compact S" unfolding seq_compact_def using assms by fast lemma seq_compactE: assumes "seq_compact S" "\n. f n \ S" obtains l r where "l \ S" "strict_mono (r :: nat \ nat)" "((f \ r) \ l) sequentially" using assms unfolding seq_compact_def by fast lemma closed_sequentially: (* TODO: move upwards *) assumes "closed s" and "\n. f n \ s" and "f \ l" shows "l \ s" proof (rule ccontr) assume "l \ s" with \closed s\ and \f \ l\ have "eventually (\n. f n \ - s) sequentially" by (fast intro: topological_tendstoD) with \\n. f n \ s\ show "False" by simp qed lemma seq_compact_Int_closed: assumes "seq_compact s" and "closed t" shows "seq_compact (s \ t)" proof (rule seq_compactI) fix f assume "\n::nat. f n \ s \ t" hence "\n. f n \ s" and "\n. f n \ t" by simp_all from \seq_compact s\ and \\n. f n \ s\ obtain l r where "l \ s" and r: "strict_mono r" and l: "(f \ r) \ l" by (rule seq_compactE) from \\n. f n \ t\ have "\n. (f \ r) n \ t" by simp from \closed t\ and this and l have "l \ t" by (rule closed_sequentially) with \l \ s\ and r and l show "\l\s \ t. \r. strict_mono r \ (f \ r) \ l" by fast qed lemma seq_compact_closed_subset: assumes "closed s" and "s \ t" and "seq_compact t" shows "seq_compact s" using assms seq_compact_Int_closed [of t s] by (simp add: Int_absorb1) lemma seq_compact_imp_countably_compact: fixes U :: "'a :: first_countable_topology set" assumes "seq_compact U" shows "countably_compact U" proof (safe intro!: countably_compactI) fix A assume A: "\a\A. open a" "U \ \A" "countable A" have subseq: "\X. range X \ U \ \r x. x \ U \ strict_mono (r :: nat \ nat) \ (X \ r) \ x" using \seq_compact U\ by (fastforce simp: seq_compact_def subset_eq) show "\T\A. finite T \ U \ \T" proof cases assume "finite A" with A show ?thesis by auto next assume "infinite A" then have "A \ {}" by auto show ?thesis proof (rule ccontr) assume "\ (\T\A. finite T \ U \ \T)" then have "\T. \x. T \ A \ finite T \ (x \ U - \T)" by auto then obtain X' where T: "\T. T \ A \ finite T \ X' T \ U - \T" by metis define X where "X n = X' (from_nat_into A ` {.. n})" for n have X: "\n. X n \ U - (\i\n. from_nat_into A i)" using \A \ {}\ unfolding X_def by (intro T) (auto intro: from_nat_into) then have "range X \ U" by auto with subseq[of X] obtain r x where "x \ U" and r: "strict_mono r" "(X \ r) \ x" by auto from \x\U\ \U \ \A\ from_nat_into_surj[OF \countable A\] obtain n where "x \ from_nat_into A n" by auto with r(2) A(1) from_nat_into[OF \A \ {}\, of n] have "eventually (\i. X (r i) \ from_nat_into A n) sequentially" unfolding tendsto_def by (auto simp: comp_def) then obtain N where "\i. N \ i \ X (r i) \ from_nat_into A n" by (auto simp: eventually_sequentially) moreover from X have "\i. n \ r i \ X (r i) \ from_nat_into A n" by auto moreover from \strict_mono r\[THEN seq_suble, of "max n N"] have "\i. n \ r i \ N \ i" by (auto intro!: exI[of _ "max n N"]) ultimately show False by auto qed qed qed lemma compact_imp_seq_compact: fixes U :: "'a :: first_countable_topology set" assumes "compact U" shows "seq_compact U" unfolding seq_compact_def proof safe fix X :: "nat \ 'a" assume "\n. X n \ U" then have "eventually (\x. x \ U) (filtermap X sequentially)" by (auto simp: eventually_filtermap) moreover have "filtermap X sequentially \ bot" by (simp add: trivial_limit_def eventually_filtermap) ultimately obtain x where "x \ U" and x: "inf (nhds x) (filtermap X sequentially) \ bot" (is "?F \ _") using \compact U\ by (auto simp: compact_filter) from countable_basis_at_decseq[of x] obtain A where A: "\i. open (A i)" "\i. x \ A i" "\S. open S \ x \ S \ eventually (\i. A i \ S) sequentially" by blast define s where "s n i = (SOME j. i < j \ X j \ A (Suc n))" for n i { fix n i have "\a. i < a \ X a \ A (Suc n)" proof (rule ccontr) assume "\ (\a>i. X a \ A (Suc n))" then have "\a. Suc i \ a \ X a \ A (Suc n)" by auto then have "eventually (\x. x \ A (Suc n)) (filtermap X sequentially)" by (auto simp: eventually_filtermap eventually_sequentially) moreover have "eventually (\x. x \ A (Suc n)) (nhds x)" using A(1,2)[of "Suc n"] by (auto simp: eventually_nhds) ultimately have "eventually (\x. False) ?F" by (auto simp: eventually_inf) with x show False by (simp add: eventually_False) qed then have "i < s n i" "X (s n i) \ A (Suc n)" unfolding s_def by (auto intro: someI2_ex) } note s = this define r where "r = rec_nat (s 0 0) s" have "strict_mono r" by (auto simp: r_def s strict_mono_Suc_iff) moreover have "(\n. X (r n)) \ x" proof (rule topological_tendstoI) fix S assume "open S" "x \ S" with A(3) have "eventually (\i. A i \ S) sequentially" by auto moreover { fix i assume "Suc 0 \ i" then have "X (r i) \ A i" by (cases i) (simp_all add: r_def s) } then have "eventually (\i. X (r i) \ A i) sequentially" by (auto simp: eventually_sequentially) ultimately show "eventually (\i. X (r i) \ S) sequentially" by eventually_elim auto qed ultimately show "\x \ U. \r. strict_mono r \ (X \ r) \ x" using \x \ U\ by (auto simp: convergent_def comp_def) qed lemma countably_compact_imp_acc_point: assumes "countably_compact s" and "countable t" and "infinite t" and "t \ s" shows "\x\s. \U. x\U \ open U \ infinite (U \ t)" proof (rule ccontr) define C where "C = (\F. interior (F \ (- t))) ` {F. finite F \ F \ t }" note \countably_compact s\ moreover have "\t\C. open t" by (auto simp: C_def) moreover assume "\ (\x\s. \U. x\U \ open U \ infinite (U \ t))" then have s: "\x. x \ s \ \U. x\U \ open U \ finite (U \ t)" by metis have "s \ \C" using \t \ s\ unfolding C_def apply (safe dest!: s) apply (rule_tac a="U \ t" in UN_I) apply (auto intro!: interiorI simp add: finite_subset) done moreover from \countable t\ have "countable C" unfolding C_def by (auto intro: countable_Collect_finite_subset) ultimately obtain D where "D \ C" "finite D" "s \ \D" by (rule countably_compactE) then obtain E where E: "E \ {F. finite F \ F \ t }" "finite E" and s: "s \ (\F\E. interior (F \ (- t)))" by (metis (lifting) finite_subset_image C_def) from s \t \ s\ have "t \ \E" using interior_subset by blast moreover have "finite (\E)" using E by auto ultimately show False using \infinite t\ by (auto simp: finite_subset) qed lemma countable_acc_point_imp_seq_compact: fixes s :: "'a::first_countable_topology set" assumes "\t. infinite t \ countable t \ t \ s \ (\x\s. \U. x\U \ open U \ infinite (U \ t))" shows "seq_compact s" proof - { fix f :: "nat \ 'a" assume f: "\n. f n \ s" have "\l\s. \r. strict_mono r \ ((f \ r) \ l) sequentially" proof (cases "finite (range f)") case True obtain l where "infinite {n. f n = f l}" using pigeonhole_infinite[OF _ True] by auto then obtain r :: "nat \ nat" where "strict_mono r" and fr: "\n. f (r n) = f l" using infinite_enumerate by blast then have "strict_mono r \ (f \ r) \ f l" by (simp add: fr o_def) with f show "\l\s. \r. strict_mono r \ (f \ r) \ l" by auto next case False with f assms have "\x\s. \U. x\U \ open U \ infinite (U \ range f)" by auto then obtain l where "l \ s" "\U. l\U \ open U \ infinite (U \ range f)" .. from this(2) have "\r. strict_mono r \ ((f \ r) \ l) sequentially" using acc_point_range_imp_convergent_subsequence[of l f] by auto with \l \ s\ show "\l\s. \r. strict_mono r \ ((f \ r) \ l) sequentially" .. qed } then show ?thesis unfolding seq_compact_def by auto qed lemma seq_compact_eq_countably_compact: fixes U :: "'a :: first_countable_topology set" shows "seq_compact U \ countably_compact U" using countable_acc_point_imp_seq_compact countably_compact_imp_acc_point seq_compact_imp_countably_compact by metis lemma seq_compact_eq_acc_point: fixes s :: "'a :: first_countable_topology set" shows "seq_compact s \ (\t. infinite t \ countable t \ t \ s --> (\x\s. \U. x\U \ open U \ infinite (U \ t)))" using countable_acc_point_imp_seq_compact[of s] countably_compact_imp_acc_point[of s] seq_compact_imp_countably_compact[of s] by metis lemma seq_compact_eq_compact: fixes U :: "'a :: second_countable_topology set" shows "seq_compact U \ compact U" using seq_compact_eq_countably_compact countably_compact_eq_compact by blast proposition Bolzano_Weierstrass_imp_seq_compact: fixes s :: "'a::{t1_space, first_countable_topology} set" shows "\t. infinite t \ t \ s \ (\x \ s. x islimpt t) \ seq_compact s" by (rule countable_acc_point_imp_seq_compact) (metis islimpt_eq_acc_point) subsection\<^marker>\tag unimportant\ \Cartesian products\ lemma seq_compact_Times: "seq_compact s \ seq_compact t \ seq_compact (s \ t)" unfolding seq_compact_def apply clarify apply (drule_tac x="fst \ f" in spec) apply (drule mp, simp add: mem_Times_iff) apply (clarify, rename_tac l1 r1) apply (drule_tac x="snd \ f \ r1" in spec) apply (drule mp, simp add: mem_Times_iff) apply (clarify, rename_tac l2 r2) apply (rule_tac x="(l1, l2)" in rev_bexI, simp) apply (rule_tac x="r1 \ r2" in exI) apply (rule conjI, simp add: strict_mono_def) apply (drule_tac f=r2 in LIMSEQ_subseq_LIMSEQ, assumption) apply (drule (1) tendsto_Pair) back apply (simp add: o_def) done lemma compact_Times: assumes "compact s" "compact t" shows "compact (s \ t)" proof (rule compactI) fix C assume C: "\t\C. open t" "s \ t \ \C" have "\x\s. \a. open a \ x \ a \ (\d\C. finite d \ a \ t \ \d)" proof fix x assume "x \ s" have "\y\t. \a b c. c \ C \ open a \ open b \ x \ a \ y \ b \ a \ b \ c" (is "\y\t. ?P y") proof fix y assume "y \ t" with \x \ s\ C obtain c where "c \ C" "(x, y) \ c" "open c" by auto then show "?P y" by (auto elim!: open_prod_elim) qed then obtain a b c where b: "\y. y \ t \ open (b y)" and c: "\y. y \ t \ c y \ C \ open (a y) \ open (b y) \ x \ a y \ y \ b y \ a y \ b y \ c y" by metis then have "\y\t. open (b y)" "t \ (\y\t. b y)" by auto with compactE_image[OF \compact t\] obtain D where D: "D \ t" "finite D" "t \ (\y\D. b y)" by metis moreover from D c have "(\y\D. a y) \ t \ (\y\D. c y)" by (fastforce simp: subset_eq) ultimately show "\a. open a \ x \ a \ (\d\C. finite d \ a \ t \ \d)" using c by (intro exI[of _ "c`D"] exI[of _ "\(a`D)"] conjI) (auto intro!: open_INT) qed then obtain a d where a: "\x. x\s \ open (a x)" "s \ (\x\s. a x)" and d: "\x. x \ s \ d x \ C \ finite (d x) \ a x \ t \ \(d x)" unfolding subset_eq UN_iff by metis moreover from compactE_image[OF \compact s\ a] obtain e where e: "e \ s" "finite e" and s: "s \ (\x\e. a x)" by auto moreover { from s have "s \ t \ (\x\e. a x \ t)" by auto also have "\ \ (\x\e. \(d x))" using d \e \ s\ by (intro UN_mono) auto finally have "s \ t \ (\x\e. \(d x))" . } ultimately show "\C'\C. finite C' \ s \ t \ \C'" by (intro exI[of _ "(\x\e. d x)"]) (auto simp: subset_eq) qed lemma tube_lemma: assumes "compact K" assumes "open W" assumes "{x0} \ K \ W" shows "\X0. x0 \ X0 \ open X0 \ X0 \ K \ W" proof - { fix y assume "y \ K" then have "(x0, y) \ W" using assms by auto with \open W\ have "\X0 Y. open X0 \ open Y \ x0 \ X0 \ y \ Y \ X0 \ Y \ W" by (rule open_prod_elim) blast } then obtain X0 Y where *: "\y \ K. open (X0 y) \ open (Y y) \ x0 \ X0 y \ y \ Y y \ X0 y \ Y y \ W" by metis from * have "\t\Y ` K. open t" "K \ \(Y ` K)" by auto with \compact K\ obtain CC where CC: "CC \ Y ` K" "finite CC" "K \ \CC" by (meson compactE) then obtain c where c: "\C. C \ CC \ c C \ K \ C = Y (c C)" by (force intro!: choice) with * CC show ?thesis by (force intro!: exI[where x="\C\CC. X0 (c C)"]) (* SLOW *) qed lemma continuous_on_prod_compactE: fixes fx::"'a::topological_space \ 'b::topological_space \ 'c::metric_space" and e::real assumes cont_fx: "continuous_on (U \ C) fx" assumes "compact C" assumes [intro]: "x0 \ U" notes [continuous_intros] = continuous_on_compose2[OF cont_fx] assumes "e > 0" obtains X0 where "x0 \ X0" "open X0" "\x\X0 \ U. \t \ C. dist (fx (x, t)) (fx (x0, t)) \ e" proof - define psi where "psi = (\(x, t). dist (fx (x, t)) (fx (x0, t)))" define W0 where "W0 = {(x, t) \ U \ C. psi (x, t) < e}" have W0_eq: "W0 = psi -` {.. U \ C" by (auto simp: vimage_def W0_def) have "open {.. C) psi" by (auto intro!: continuous_intros simp: psi_def split_beta') from this[unfolded continuous_on_open_invariant, rule_format, OF \open {..] obtain W where W: "open W" "W \ U \ C = W0 \ U \ C" unfolding W0_eq by blast have "{x0} \ C \ W \ U \ C" unfolding W by (auto simp: W0_def psi_def \0 < e\) then have "{x0} \ C \ W" by blast from tube_lemma[OF \compact C\ \open W\ this] obtain X0 where X0: "x0 \ X0" "open X0" "X0 \ C \ W" by blast have "\x\X0 \ U. \t \ C. dist (fx (x, t)) (fx (x0, t)) \ e" proof safe fix x assume x: "x \ X0" "x \ U" fix t assume t: "t \ C" have "dist (fx (x, t)) (fx (x0, t)) = psi (x, t)" by (auto simp: psi_def) also { have "(x, t) \ X0 \ C" using t x by auto also note \\ \ W\ finally have "(x, t) \ W" . with t x have "(x, t) \ W \ U \ C" by blast also note \W \ U \ C = W0 \ U \ C\ finally have "psi (x, t) < e" by (auto simp: W0_def) } finally show "dist (fx (x, t)) (fx (x0, t)) \ e" by simp qed from X0(1,2) this show ?thesis .. qed subsection \Continuity\ lemma continuous_at_imp_continuous_within: "continuous (at x) f \ continuous (at x within s) f" unfolding continuous_within continuous_at using Lim_at_imp_Lim_at_within by auto lemma Lim_trivial_limit: "trivial_limit net \ (f \ l) net" by simp lemmas continuous_on = continuous_on_def \ \legacy theorem name\ lemma continuous_within_subset: "continuous (at x within s) f \ t \ s \ continuous (at x within t) f" unfolding continuous_within by(metis tendsto_within_subset) lemma continuous_on_interior: "continuous_on s f \ x \ interior s \ continuous (at x) f" by (metis continuous_on_eq_continuous_at continuous_on_subset interiorE) lemma continuous_on_eq: "\continuous_on s f; \x. x \ s \ f x = g x\ \ continuous_on s g" unfolding continuous_on_def tendsto_def eventually_at_topological by simp text \Characterization of various kinds of continuity in terms of sequences.\ lemma continuous_within_sequentiallyI: fixes f :: "'a::{first_countable_topology, t2_space} \ 'b::topological_space" assumes "\u::nat \ 'a. u \ a \ (\n. u n \ s) \ (\n. f (u n)) \ f a" shows "continuous (at a within s) f" using assms unfolding continuous_within tendsto_def[where l = "f a"] by (auto intro!: sequentially_imp_eventually_within) lemma continuous_within_tendsto_compose: fixes f::"'a::t2_space \ 'b::topological_space" assumes "continuous (at a within s) f" "eventually (\n. x n \ s) F" "(x \ a) F " shows "((\n. f (x n)) \ f a) F" proof - have *: "filterlim x (inf (nhds a) (principal s)) F" using assms(2) assms(3) unfolding at_within_def filterlim_inf by (auto simp: filterlim_principal eventually_mono) show ?thesis by (auto simp: assms(1) continuous_within[symmetric] tendsto_at_within_iff_tendsto_nhds[symmetric] intro!: filterlim_compose[OF _ *]) qed lemma continuous_within_tendsto_compose': fixes f::"'a::t2_space \ 'b::topological_space" assumes "continuous (at a within s) f" "\n. x n \ s" "(x \ a) F " shows "((\n. f (x n)) \ f a) F" by (auto intro!: continuous_within_tendsto_compose[OF assms(1)] simp add: assms) lemma continuous_within_sequentially: fixes f :: "'a::{first_countable_topology, t2_space} \ 'b::topological_space" shows "continuous (at a within s) f \ (\x. (\n::nat. x n \ s) \ (x \ a) sequentially \ ((f \ x) \ f a) sequentially)" using continuous_within_tendsto_compose'[of a s f _ sequentially] continuous_within_sequentiallyI[of a s f] by (auto simp: o_def) lemma continuous_at_sequentiallyI: fixes f :: "'a::{first_countable_topology, t2_space} \ 'b::topological_space" assumes "\u. u \ a \ (\n. f (u n)) \ f a" shows "continuous (at a) f" using continuous_within_sequentiallyI[of a UNIV f] assms by auto lemma continuous_at_sequentially: fixes f :: "'a::metric_space \ 'b::topological_space" shows "continuous (at a) f \ (\x. (x \ a) sequentially --> ((f \ x) \ f a) sequentially)" using continuous_within_sequentially[of a UNIV f] by simp lemma continuous_on_sequentiallyI: fixes f :: "'a::{first_countable_topology, t2_space} \ 'b::topological_space" assumes "\u a. (\n. u n \ s) \ a \ s \ u \ a \ (\n. f (u n)) \ f a" shows "continuous_on s f" using assms unfolding continuous_on_eq_continuous_within using continuous_within_sequentiallyI[of _ s f] by auto lemma continuous_on_sequentially: fixes f :: "'a::{first_countable_topology, t2_space} \ 'b::topological_space" shows "continuous_on s f \ (\x. \a \ s. (\n. x(n) \ s) \ (x \ a) sequentially --> ((f \ x) \ f a) sequentially)" (is "?lhs = ?rhs") proof assume ?rhs then show ?lhs using continuous_within_sequentially[of _ s f] unfolding continuous_on_eq_continuous_within by auto next assume ?lhs then show ?rhs unfolding continuous_on_eq_continuous_within using continuous_within_sequentially[of _ s f] by auto qed text \Continuity in terms of open preimages.\ lemma continuous_at_open: "continuous (at x) f \ (\t. open t \ f x \ t --> (\s. open s \ x \ s \ (\x' \ s. (f x') \ t)))" unfolding continuous_within_topological [of x UNIV f] unfolding imp_conjL by (intro all_cong imp_cong ex_cong conj_cong refl) auto lemma continuous_imp_tendsto: assumes "continuous (at x0) f" and "x \ x0" shows "(f \ x) \ (f x0)" proof (rule topological_tendstoI) fix S assume "open S" "f x0 \ S" then obtain T where T_def: "open T" "x0 \ T" "\x\T. f x \ S" using assms continuous_at_open by metis then have "eventually (\n. x n \ T) sequentially" using assms T_def by (auto simp: tendsto_def) then show "eventually (\n. (f \ x) n \ S) sequentially" using T_def by (auto elim!: eventually_mono) qed subsection \Homeomorphisms\ definition\<^marker>\tag important\ "homeomorphism s t f g \ (\x\s. (g(f x) = x)) \ (f ` s = t) \ continuous_on s f \ (\y\t. (f(g y) = y)) \ (g ` t = s) \ continuous_on t g" lemma homeomorphismI [intro?]: assumes "continuous_on S f" "continuous_on T g" "f ` S \ T" "g ` T \ S" "\x. x \ S \ g(f x) = x" "\y. y \ T \ f(g y) = y" shows "homeomorphism S T f g" using assms by (force simp: homeomorphism_def) lemma homeomorphism_translation: fixes a :: "'a :: real_normed_vector" shows "homeomorphism ((+) a ` S) S ((+) (- a)) ((+) a)" unfolding homeomorphism_def by (auto simp: algebra_simps continuous_intros) lemma homeomorphism_ident: "homeomorphism T T (\a. a) (\a. a)" by (rule homeomorphismI) auto lemma homeomorphism_compose: assumes "homeomorphism S T f g" "homeomorphism T U h k" shows "homeomorphism S U (h o f) (g o k)" using assms unfolding homeomorphism_def by (intro conjI ballI continuous_on_compose) (auto simp: image_iff) lemma homeomorphism_cong: "homeomorphism X' Y' f' g'" if "homeomorphism X Y f g" "X' = X" "Y' = Y" "\x. x \ X \ f' x = f x" "\y. y \ Y \ g' y = g y" using that by (auto simp add: homeomorphism_def) lemma homeomorphism_empty [simp]: "homeomorphism {} {} f g" unfolding homeomorphism_def by auto lemma homeomorphism_symD: "homeomorphism S t f g \ homeomorphism t S g f" by (simp add: homeomorphism_def) lemma homeomorphism_sym: "homeomorphism S t f g = homeomorphism t S g f" by (force simp: homeomorphism_def) definition\<^marker>\tag important\ homeomorphic :: "'a::topological_space set \ 'b::topological_space set \ bool" (infixr "homeomorphic" 60) where "s homeomorphic t \ (\f g. homeomorphism s t f g)" lemma homeomorphic_empty [iff]: "S homeomorphic {} \ S = {}" "{} homeomorphic S \ S = {}" by (auto simp: homeomorphic_def homeomorphism_def) lemma homeomorphic_refl: "s homeomorphic s" unfolding homeomorphic_def homeomorphism_def using continuous_on_id apply (rule_tac x = "(\x. x)" in exI) apply (rule_tac x = "(\x. x)" in exI) apply blast done lemma homeomorphic_sym: "s homeomorphic t \ t homeomorphic s" unfolding homeomorphic_def homeomorphism_def by blast lemma homeomorphic_trans [trans]: assumes "S homeomorphic T" and "T homeomorphic U" shows "S homeomorphic U" using assms unfolding homeomorphic_def by (metis homeomorphism_compose) lemma homeomorphic_minimal: "s homeomorphic t \ (\f g. (\x\s. f(x) \ t \ (g(f(x)) = x)) \ (\y\t. g(y) \ s \ (f(g(y)) = y)) \ continuous_on s f \ continuous_on t g)" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs by (fastforce simp: homeomorphic_def homeomorphism_def) next assume ?rhs then show ?lhs apply clarify unfolding homeomorphic_def homeomorphism_def by (metis equalityI image_subset_iff subsetI) qed lemma homeomorphicI [intro?]: "\f ` S = T; g ` T = S; continuous_on S f; continuous_on T g; \x. x \ S \ g(f(x)) = x; \y. y \ T \ f(g(y)) = y\ \ S homeomorphic T" unfolding homeomorphic_def homeomorphism_def by metis lemma homeomorphism_of_subsets: "\homeomorphism S T f g; S' \ S; T'' \ T; f ` S' = T'\ \ homeomorphism S' T' f g" apply (auto simp: homeomorphism_def elim!: continuous_on_subset) by (metis subsetD imageI) lemma homeomorphism_apply1: "\homeomorphism S T f g; x \ S\ \ g(f x) = x" by (simp add: homeomorphism_def) lemma homeomorphism_apply2: "\homeomorphism S T f g; x \ T\ \ f(g x) = x" by (simp add: homeomorphism_def) lemma homeomorphism_image1: "homeomorphism S T f g \ f ` S = T" by (simp add: homeomorphism_def) lemma homeomorphism_image2: "homeomorphism S T f g \ g ` T = S" by (simp add: homeomorphism_def) lemma homeomorphism_cont1: "homeomorphism S T f g \ continuous_on S f" by (simp add: homeomorphism_def) lemma homeomorphism_cont2: "homeomorphism S T f g \ continuous_on T g" by (simp add: homeomorphism_def) lemma continuous_on_no_limpt: "(\x. \ x islimpt S) \ continuous_on S f" unfolding continuous_on_def by (metis UNIV_I empty_iff eventually_at_topological islimptE open_UNIV tendsto_def trivial_limit_within) lemma continuous_on_finite: fixes S :: "'a::t1_space set" shows "finite S \ continuous_on S f" by (metis continuous_on_no_limpt islimpt_finite) lemma homeomorphic_finite: fixes S :: "'a::t1_space set" and T :: "'b::t1_space set" assumes "finite T" shows "S homeomorphic T \ finite S \ finite T \ card S = card T" (is "?lhs = ?rhs") proof assume "S homeomorphic T" with assms show ?rhs apply (auto simp: homeomorphic_def homeomorphism_def) apply (metis finite_imageI) by (metis card_image_le finite_imageI le_antisym) next assume R: ?rhs with finite_same_card_bij obtain h where "bij_betw h S T" by auto with R show ?lhs apply (auto simp: homeomorphic_def homeomorphism_def continuous_on_finite) apply (rule_tac x=h in exI) apply (rule_tac x="inv_into S h" in exI) apply (auto simp: bij_betw_inv_into_left bij_betw_inv_into_right bij_betw_imp_surj_on inv_into_into bij_betwE) apply (metis bij_betw_def bij_betw_inv_into) done qed text \Relatively weak hypotheses if a set is compact.\ lemma homeomorphism_compact: fixes f :: "'a::topological_space \ 'b::t2_space" assumes "compact s" "continuous_on s f" "f ` s = t" "inj_on f s" shows "\g. homeomorphism s t f g" proof - define g where "g x = (SOME y. y\s \ f y = x)" for x have g: "\x\s. g (f x) = x" using assms(3) assms(4)[unfolded inj_on_def] unfolding g_def by auto { fix y assume "y \ t" then obtain x where x:"f x = y" "x\s" using assms(3) by auto then have "g (f x) = x" using g by auto then have "f (g y) = y" unfolding x(1)[symmetric] by auto } then have g':"\x\t. f (g x) = x" by auto moreover { fix x have "x\s \ x \ g ` t" using g[THEN bspec[where x=x]] unfolding image_iff using assms(3) by (auto intro!: bexI[where x="f x"]) moreover { assume "x\g ` t" then obtain y where y:"y\t" "g y = x" by auto then obtain x' where x':"x'\s" "f x' = y" using assms(3) by auto then have "x \ s" unfolding g_def using someI2[of "\b. b\s \ f b = y" x' "\x. x\s"] unfolding y(2)[symmetric] and g_def by auto } ultimately have "x\s \ x \ g ` t" .. } then have "g ` t = s" by auto ultimately show ?thesis unfolding homeomorphism_def homeomorphic_def - apply (rule_tac x=g in exI) - using g and assms(3) and continuous_on_inv[OF assms(2,1), of g, unfolded assms(3)] and assms(2) - apply auto - done + using assms continuous_on_inv by fastforce qed lemma homeomorphic_compact: fixes f :: "'a::topological_space \ 'b::t2_space" shows "compact s \ continuous_on s f \ (f ` s = t) \ inj_on f s \ s homeomorphic t" unfolding homeomorphic_def by (metis homeomorphism_compact) text\Preservation of topological properties.\ lemma homeomorphic_compactness: "s homeomorphic t \ (compact s \ compact t)" unfolding homeomorphic_def homeomorphism_def by (metis compact_continuous_image) subsection\<^marker>\tag unimportant\ \On Linorder Topologies\ lemma islimpt_greaterThanLessThan1: fixes a b::"'a::{linorder_topology, dense_order}" assumes "a < b" shows "a islimpt {a<.. T" from open_right[OF this \a < b\] obtain c where c: "a < c" "{a.. T" by auto with assms dense[of a "min c b"] show "\y\{a<.. T \ y \ a" by (metis atLeastLessThan_iff greaterThanLessThan_iff min_less_iff_conj not_le order.strict_implies_order subset_eq) qed lemma islimpt_greaterThanLessThan2: fixes a b::"'a::{linorder_topology, dense_order}" assumes "a < b" shows "b islimpt {a<.. T" from open_left[OF this \a < b\] obtain c where c: "c < b" "{c<..b} \ T" by auto with assms dense[of "max a c" b] show "\y\{a<.. T \ y \ b" by (metis greaterThanAtMost_iff greaterThanLessThan_iff max_less_iff_conj not_le order.strict_implies_order subset_eq) qed lemma closure_greaterThanLessThan[simp]: fixes a b::"'a::{linorder_topology, dense_order}" shows "a < b \ closure {a <..< b} = {a .. b}" (is "_ \ ?l = ?r") proof have "?l \ closure ?r" by (rule closure_mono) auto thus "closure {a<.. {a..b}" by simp qed (auto simp: closure_def order.order_iff_strict islimpt_greaterThanLessThan1 islimpt_greaterThanLessThan2) lemma closure_greaterThan[simp]: fixes a b::"'a::{no_top, linorder_topology, dense_order}" shows "closure {a<..} = {a..}" proof - from gt_ex obtain b where "a < b" by auto hence "{a<..} = {a<.. {b..}" by auto also have "closure \ = {a..}" using \a < b\ unfolding closure_Un by auto finally show ?thesis . qed lemma closure_lessThan[simp]: fixes b::"'a::{no_bot, linorder_topology, dense_order}" shows "closure {.. {..a}" by auto also have "closure \ = {..b}" using \a < b\ unfolding closure_Un by auto finally show ?thesis . qed lemma closure_atLeastLessThan[simp]: fixes a b::"'a::{linorder_topology, dense_order}" assumes "a < b" shows "closure {a ..< b} = {a .. b}" proof - from assms have "{a ..< b} = {a} \ {a <..< b}" by auto also have "closure \ = {a .. b}" unfolding closure_Un by (auto simp: assms less_imp_le) finally show ?thesis . qed lemma closure_greaterThanAtMost[simp]: fixes a b::"'a::{linorder_topology, dense_order}" assumes "a < b" shows "closure {a <.. b} = {a .. b}" proof - from assms have "{a <.. b} = {b} \ {a <..< b}" by auto also have "closure \ = {a .. b}" unfolding closure_Un by (auto simp: assms less_imp_le) finally show ?thesis . qed end \ No newline at end of file