(* 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 \<open>Abstract Topology 2\<close>
theory Abstract_Topology_2 imports
Elementary_Topology Abstract_Topology Continuum_Not_Denumerable "HOL-Library.Indicator_Function" "HOL-Library.Equipollence" begin
text\<open>Combination of Elementary and Abstract Topology\<close>
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)" by (meson dense less_eq_real_def order_le_less_trans)
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 \
(\<exists>U::'a set. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> V))" by auto show False proof (cases "x \ A") assume x: "x \ A" hence"indicator A x \ ({0<..<2} :: real set)" by simp with 1 obtain U where U: "open U""x \ U" "\y\U. indicator A y \ ({0<..<2} :: real set)" using open_greaterThanLessThan by metis 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 with 1 obtain U where U: "open U""x \ U" "\y\U. indicator A y \ ({-1<..<1} :: real set)" using 1 open_greaterThanLessThan by metis 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" thenobtain 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)" thenobtain U where U: "open U""x \ U" "U \ -A" unfolding interior_def by auto thenhave"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 islimpt_closure: "\S \ T; \x. \x islimpt S; x \ T\ \ x \ S\ \ S = T \ closure S" using closure_def by fastforce
lemma closedin_limpt: "closedin (top_of_set T) S \ S \ T \ (\x. x islimpt S \ x \ T \ x \ S)" proof - have"\U x. \closed U; S = T \ U; x islimpt S; x \ T\ \ x \ S" by (meson IntI closed_limpt inf_le2 islimpt_subset) thenshow ?thesis by (metis closed_closure closedin_closed closedin_imp_subset islimpt_closure) qed
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 \<Longrightarrow> connected S \<longleftrightarrow> (\<nexists>A B. closed A \<and> closed B \<and> A \<noteq> {} \<and> B \<noteq> {} \<and> A \<union> B = S \<and> A \<inter> B = {})" unfolding connected_closedin_eq closedin_closed_eq connected_closedin_eq by blast
text\<open>If a connnected set is written as the union of two nonempty closed sets, then these sets haveto intersect.\<close>
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_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 \<open>Closure\<close>
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)" unfolding S proof fix x assume"x \ closure (U \ V \ closure T)" thenhave"V \ closure T \ A \ x \ closure A" for A by (metis closure_mono subsetD inf.coboundedI2 inf_assoc) thenhave"x \ closure (T \ V)" by (metis \<open>open V\<close> closure_closure inf_commute open_Int_closure_subset) thenshow"x \ closure (U \ V \ T)" by (metis \<open>T \<subseteq> U\<close> 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 = {}" thenhave"openin (top_of_set S) (A \ V \ S)" by (simp add: inf_absorb2 openin_subtopology_Int) moreoverhave"A \ V \ S \ {}" using \x \ V\ \V \ A\ \x \ S\ by auto ultimatelyshow False using\<open>T \<inter> A = {}\<close> assms by fastforce qed
subsection \<open>Frontier\<close>
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: assumes"connected S" and"S \ T \ {}" and"S - T \ {}" shows"S \ frontier T \ {}" proof - have"openin (top_of_set S) (S \ interior T)" "openin (top_of_set S) (S \ interior (-T))" by blast+ thenshow ?thesis using\<open>connected S\<close> [unfolded connected_openin] by (metis assms connectedin_Int_frontier_of connectedin_iff_connected euclidean_frontier_of) qed
subsection \<open>Compactness\<close>
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 \
(\<forall>C. (\<forall>c\<in>C. openin (top_of_set S) c) \<and> S \<subseteq> \<Union>C \<longrightarrow>
(\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D))" proof safe fix C assume"compact S"and"\c\C. openin (top_of_set S) c" and "S \ \C" thenhave"\c\{T. open T \ S \ T \ C}. open c" and "S \ \{T. open T \ S \ T \ C}" unfolding openin_open by force+ with\<open>compact S\<close> obtain D where "D \<subseteq> {T. open T \<and> S \<inter> T \<in> C}" and "finite D" and "S \<subseteq> \<Union>D" by (meson compactE) thenhave"image (\T. S \ T) D \ C \ finite (image (\T. S \ T) D) \ S \ \(image (\T. S \ T) D)" by auto thenshow"\D\C. finite D \ S \ \D" .. next assume 1: "\C. (\c\C. openin (top_of_set S) c) \ S \ \C \
(\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D)" show"compact S" proof (rule compactI) fix C let ?C = "image (\T. S \ T) C" assume"\t\C. open t" and "S \ \C" thenhave"(\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\<open>D \<subseteq> ?C\<close> show "?D \<subseteq> C" by (fast intro: inv_into_into) from\<open>finite D\<close> show "finite ?D" by (rule finite_imageI) from\<open>S \<subseteq> \<Union>D\<close> show "S \<subseteq> \<Union>?D" by (metis \<open>D \<subseteq> (\<inter>) S ` C\<close> image_inv_into_cancel inf_Sup le_infE) qed thenshow"\D\C. finite D \ S \ \D" .. qed qed
subsection \<open>Continuity\<close>
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)" thenobtain T where as: "open T""x \ T" "T \ f ` S" .. thenhave"x \ f ` S" by auto thenobtain y where y: "y \ S" "x = f y" by auto have"open (f -` T)" using assms \<open>open T\<close> by (simp add: continuous_at_imp_continuous_on open_vimage) moreoverhave"y \ vimage f T" using\<open>x = f y\<close> \<open>x \<in> T\<close> by simp moreoverhave"vimage f T \ S" using\<open>T \<subseteq> image f S\<close> \<open>inj f\<close> unfolding inj_on_def subset_eq by auto ultimatelyhave"y \ interior S" .. with\<open>x = f y\<close> show "x \<in> f ` interior S" .. qed
subsection\<^marker>\<open>tag unimportant\<close> \<open>Equality of continuous functions on closure and related results\<close>
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 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 moreoverhave"closed (closure S \ f -` T)" using continuous_closed_preimage[OF contf] \<open>closed T\<close> by auto ultimatelyhave"closure S = (closure S \ f -` T)" using closure_minimal[of S "(closure S \ f -` T)"] by auto thenshow ?thesis by auto qed
lemma continuous_image_closure_subset: assumes"continuous_on A f""closure B \ A" shows"f ` closure B \ closure (f ` B)" using assms by (meson closed_closure closure_subset continuous_on_subset image_closure_subset)
subsection\<^marker>\<open>tag unimportant\<close> \<open>A function constant on a set\<close>
definition constant_on (infixl\<open>(constant'_on)\<close> 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_compose: assumes"f constant_on A" shows"g \ f constant_on A" using assms by (auto simp: constant_on_def)
lemma not_constant_onI: "f x \ f y \ x \ A \ y \ A \ \f constant_on A" unfolding constant_on_def by metis
lemma constant_onE: assumes"f constant_on S"and"\x. x\S \ f x = g x" shows"g constant_on S" using assms unfolding constant_on_def by simp
subsection\<^marker>\<open>tag unimportant\<close> \<open>Continuity relative to a union.\<close>
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\<rbrakk> \<Longrightarrow> continuous_on (S \<union> T) f" unfolding continuous_on closedin_limpt by (metis Lim_trivial_limit Lim_within_Un 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; \<And>x. \<lbrakk>x \<in> S \<and> \<not>P x \<or> x \<in> T \<and> P x\<rbrakk> \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> continuous_on (S \<union> T) (\<lambda>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 {x \ S. h x \ a} f" and"continuous_on {x \ S. a \ h x} g" and h: "continuous_on S h" and"\x. \x \ S; h x = a\ \ f x = g x" shows"continuous_on S (\x. if h x \ a then f(x) else g(x))" 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 [simp]: "S \ h -` {..a} = {x \ S. h x \ a}" "S \ h -` {a..} = {x \ S. a \ h x}" by auto have"continuous_on (S \ h -` {..a} \ S \ h -` {a..}) (\x. if h x \ a then f x else g x)" by (intro continuous_on_cases_local) (use 1 2 S assms in auto) thenshow ?thesis using S by force 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>\<open>tag unimportant\<close>\<open>Inverse function property for open/closed maps\<close>
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 moreoverhave"g ` T = S" by (metis hom homeomorphism_def) ultimatelyshow ?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 moreoverhave"g ` T = S" by (metis hom homeomorphism_def) ultimatelyshow ?thesis by (simp add: continuous_on_closed oo) qed
lemma subset_second_countable: obtains\<B> :: "'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\<B> :: "'a set set" where"countable \" and opeB: "\C. C \ \ \ openin(top_of_set S) C" and\<B>: "\<And>T. openin(top_of_set S) T \<Longrightarrow> \<exists>\<U>. \<U> \<subseteq> \<B> \<and> T = \<Union>\<U>" proof - obtain\<C> :: "'a set set" where"countable \" and ope: "\C. C \ \ \ open C" and\<C>: "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<C> \<and> S = \<Union>U" by (metis univ_second_countable that) show ?thesis proof show"countable ((\C. S \ C) ` \)" by (simp add: \<open>countable \<C>\<close>) 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 \<C> image_mono inf_Sup openin_open) qed qed show ?thesis proof show"countable (\ - {{}})" using\<open>countable \<B>\<close> by blast show"\C. \C \ \ - {{}}\ \ openin (top_of_set S) C" by (simp add: \<open>\<And>C. C \<in> \<B> \<Longrightarrow> openin (top_of_set S) C\<close>) show"\\\\ - {{}}. T = \\" if "openin (top_of_set S) T" for T using\<B> [OF that] by (metis Int_Diff Int_lower2 Union_insert inf.orderE insert_Diff_single sup_bot_left) qed auto qed
lemma Lindelof_openin: fixes\<F> :: "'a::second_countable_topology set set" assumes"\S. S \ \ \ openin (top_of_set U) S" obtains\<F>' where "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>" proof - have"\S. S \ \ \ \T. open T \ S = U \ T" using assms by (simp add: openin_open) thenobtain tf where tf: "\S. S \ \ \ open (tf S) \ (S = U \ tf S)" by metis have [simp]: "\\'. \' \ \ \ \\' = U \ \(tf ` \')" using tf by fastforce obtain\<G> where "countable \<G> \<and> \<G> \<subseteq> tf ` \<F>" "\<Union>\<G> = \<Union>(tf ` \<F>)" using tf by (force intro: Lindelof [of "tf ` \"]) thenobtain\<F>' where \<F>': "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>" by (clarsimp simp add: countable_subset_image) thenshow ?thesis .. qed
lemma quotient_map_imp_continuous_open: assumes T: "f \ S \ T" and ope: "\U. U \ T \<Longrightarrow> (openin (top_of_set S) (S \<inter> f -` U) \<longleftrightarrow> openin (top_of_set T) U)" shows"continuous_on S f" proof - have [simp]: "S \ f -` f ` S = S" by auto show ?thesis 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 \<Longrightarrow> (closedin (top_of_set S) (S \<inter> f -` U) \<longleftrightarrow>
closedin (top_of_set T) U)" shows"continuous_on S f" proof - have [simp]: "S \ f -` f ` S = S" by auto show ?thesis 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 \<Longrightarrow> 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 thenshow ?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 \<Longrightarrow> 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 thenhave *: "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 \<inter> f -` Z)" and g: "\Z. openin (top_of_set (g ` T)) Z \
openin (top_of_set T) (T \<inter> 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 alsohave"... = U" using U by auto finallyhave eq: "T \ g -` (g ` T \ (S \ f -` U)) = U" . assume ?lhs thenhave *: "openin (top_of_set (g ` T)) (g ` T \ (S \ f -` U))" by (metis image_subset_iff_funcset img inf_left_idem openin_subtopology_Int_subset) show ?rhs using g [OF *] eq by auto qed (use assms continuous_openin_preimage in blast) 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" using assms by (intro continuous_right_inverse_imp_quotient_map) auto
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 (simp add: assms closed_map_imp_quotient_map continuous_imp_closed_map)
subsection\<^marker>\<open>tag unimportant\<close>\<open>Pasting lemmas for functions, for of casewise definitions\<close>
subsubsection\<open>on open sets\<close>
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) thenshow"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" have"\x. x \ topspace X \ \<exists>j. j \<in> I \<and> x \<in> T j \<and> f (SOME i. i \<in> I \<and> x \<in> T i) x = f j x" by (metis (no_types, lifting) UN_E X subsetD someI_ex) with f show"continuous_map X Y ?h" by (smt (verit, best) cont ope pasting_lemma) 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 \ {}} \<subseteq> (\<lambda>i. T i \<inter> f i -` U) ` {i \<in> I. T i \<inter> V \<noteq> {}}" for V by auto have 1: "(\i\I. T i \ f i -` U) \ topspace X" using T by blast thenhave"locally_finite_in X ((\i. T i \ f i -` U) ` I)" unfolding locally_finite_in_def using finite_subset [OF sub] fin by force thenshow"closedin X (topspace X \ g -` U)" by (smt (verit, best) * cTf closedin_locally_finite_Union image_iff) qed
subsubsection\<open>Likewise on closed sets, with a finiteness assumption\<close>
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 have"\x. x \ topspace X \ \<exists>j. j \<in> I \<and> x \<in> T j \<and> f (SOME i. i \<in> I \<and> x \<in> T i) x = f j x" by (metis (no_types, lifting) UN_E X subsetD someI_ex) thenshow"continuous_map X Y (\x. f(@i. i \ I \ x \ T i) x)" by (smt (verit, best) clo cont f pasting_lemma_locally_finite [OF fin]) next fix x i assume"i \ I" and "x \ topspace X \ T i" thenshow"f (SOME i. i \ I \ x \ T i) x = f i x" by (metis (mono_tags, lifting) IntE IntI f someI2) 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 have"\x. x \ topspace X \ \<exists>j. j \<in> I \<and> x \<in> T j \<and> f (SOME i. i \<in> I \<and> x \<in> T i) x = f j x" by (metis (mono_tags, lifting) UN_iff X someI_ex subset_iff) with pasting_lemma_closed [OF \<open>finite I\<close> clo cont] show"continuous_map X Y (\x. f (SOME i. i \ I \ x \ T i) x)" by (simp add: f) next fix x i assume"i \ I" "x \ topspace X \ T i" thenshow"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" by (smt (verit, best) Diff_Diff_Int closure_of_interior_of closure_of_restrict eq fg
frontier_of_closures interior_of_complement that x) moreover have"g x = f x" if"x \ X closure_of {x. \ P x}" "x \ X closure_of Collect P" "\ i" "j" for x by (metis IntI closure_of_restrict eq fg frontier_of_closures that) ultimatelyshow ?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 by simp (metis in_closure_of 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)" proof (rule continuous_map_cases) show"continuous_map (subtopology X (X closure_of {x. P x})) Y f" by (metis Collect_conj_eq Collect_mem_eq closure_of_restrict f) next show"continuous_map (subtopology X (X closure_of {x. \ P x})) Y g" by (metis Collect_conj_eq Collect_mem_eq closure_of_restrict g) next fix x assume"x \ X frontier_of {x. P x}" thenshow"f x = g x" by (metis Collect_conj_eq Collect_mem_eq fg frontier_of_restrict) qed
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}" by (smt (verit) Collect_mono_iff DiffI closure_of_mono continuous_map contp image_subset_iff) thenshow"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 \<open>Retractions\<close>
definition\<^marker>\<open>tag important\<close> retraction :: "('a::topological_space) set \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" where"retraction S T r \
T \<subseteq> S \<and> continuous_on S r \<and> r \<in> S \<rightarrow> T \<and> (\<forall>x\<in>T. r x = x)"
definition\<^marker>\<open>tag important\<close> retract_of (infixl \<open>retract'_of\<close> 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\<open>Preservation of fixpoints under (more general notion of) retraction\<close>
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 (metis assms(4) assms(8) contg continuous_on_compose continuous_on_subset contr contt funcset_image) show"(i \ g \ r) \ S \ S" using assms(2,4,8) by force qed thenobtain x where x: "x \ S" "(i \ g \ r) x = x" .. thenhave *: "g (r x) \ T" using assms(4,8) by auto have"r ((i \ g \ r) x) = r x" using x by auto thenshow ?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)) \
(\<forall>g. continuous_on T g \<and> g \<in> T \<rightarrow> T \<longrightarrow> (\<exists>y\<in>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 Pi_I' imageI invertible_fixpoint_property[of T i S r] show ?rhs by metis next assume ?rhs with r show ?lhs using invertible_fixpoint_property[of S r T i] by (metis image_subset_iff_funcset subset_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 .. thenshow ?thesis unfolding retraction_def using invertible_fixpoint_property[OF continuous_on_id _ _ _ _ FP] by (smt (verit, del_insts) Pi_iff assms(4) contg subsetD 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 simp flip: image_subset_iff_funcset)
lemma retractionE: \<comment> \<open>yields properties normalized wrt. simp -- less likely to loop\<close> 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 thenshow"r \ S \ S" "continuous_on S r" by auto thenshow"T = r ` S" using\<open>r ` S = T\<close> by blast from\<open>\<forall>x \<in> T. r x = x\<close> have "r x = x" if "x \<in> T" for x using that by simp with\<open>r ` S = T\<close> show "r (r x) = r x" if "x \<in> S" for x using that by auto qed
lemma retract_ofE: \<comment> \<open>yields properties normalized wrt. simp -- less likely to loop\<close> 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\<open>S retract_of T\<close> obtain r where r: "retraction T S r" by (auto simp add: retract_of_def) show thesis proof show"continuous_on T (f \ r)" by (metis assms(2) continuous_on_compose retraction r) show"f \ r \ T \ U" by (metis \<open>f \<in> S \<rightarrow> U\<close> image_comp image_subset_iff_funcset r retractionE) show"\x. x \ S \ (f \ r) x = f x" by (metis comp_apply r retraction) qed 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 funcset_image 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 image_subset_iff_funcset 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 (simp add: retraction ) by (metis subset_eq continuous_on_compose2 image_image)
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 force alsohave"\ = T \ ((\x. (x, r x)) -` ({y. \x. y = (x, x)}))" unfolding vimage_def mem_Times_iff fst_conv snd_conv using r by auto alsohave"closedin (top_of_set T) \" by (rule continuous_closedin_preimage) (auto intro!: closed_diagonal continuous_on_Pair r) finallyshow ?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: assumes r: "retraction S T r"and"U \ T" shows"openin (top_of_set S) (S \ r -` U) \ openin (top_of_set T) U" (is "?lhs = ?rhs") proof assume L: ?lhs have"openin (top_of_set T) (T \ r -` U) = openin (top_of_set (r ` T)) U" using continuous_left_inverse_imp_quotient_map [of T r r U] by (metis (no_types, opaque_lifting) \<open>U \<subseteq> T\<close> equalityD1 r retraction
retraction_subset) with L show"?rhs" by (metis openin_subtopology_Int_subset order_refl r retraction retraction_subset) next show"?rhs \ ?lhs" by (metis continuous_on_open r retraction) qed
subsection\<open>Retractions on a topological space\<close>
definition retract_of_space :: "'a set \ 'a topology \ bool" (infix \retract'_of'_space\ 50) where"S retract_of_space X \<equiv> S \<subseteq> topspace X \<and> (\<exists>r. continuous_map X (subtopology X S) r \<and> (\<forall>x \<in> 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 \ X = trivial_topology" by (auto simp: 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 thenshow ?thesis by (force simp: retract_of_space_def) qed
lemma retract_of_space_trans: assumes"S retract_of_space X""T retract_of_space subtopology X S" shows"T retract_of_space X" using assms unfolding retract_of_space_retraction_maps by (metis comp_id inf.absorb_iff2 retraction_maps_compose subtopology_subtopology
topspace_subtopology)
lemma retract_of_space_subtopology: assumes"S retract_of_space X""S \ U" shows"S retract_of_space subtopology X U" using assms unfolding retract_of_space_def by (metis continuous_map_from_subtopology inf.absorb_iff2 subtopology_subtopology
topspace_subtopology)
lemma retract_of_space_clopen: assumes"openin X S""closedin X S""S = {} \ X = trivial_topology" shows"S retract_of_space X" proof (cases "S = {}") case False thenobtain 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\<open>S \<subseteq> topspace X\<close> \<open>a \<in> S\<close> 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 thenshow"continuous_map X (subtopology X S) (\x. if x \ S then x else a)" using\<open>S \<subseteq> topspace X\<close> \<open>a \<in> S\<close> 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 = {} \ X = trivial_topology" shows"S retract_of_space X" by (metis assms retract_of_space_clopen separatedin_open_sets
separation_closedin_Un_gen subtopology_topspace)
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 \<Longrightarrow> 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
lemma hereditary_imp_retractive_property: assumes"\X S. P X \ P(subtopology X S)" "\X X'. X homeomorphic_space X' \ (P X \ Q X')" assumes"retraction_map X X' r""P X" shows"Q X'" by (meson assms retraction_map_def retraction_maps_section_image2)
subsection\<open>Paths and path-connectedness\<close>
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 [simp]: "pathin X (\x. a) \ a \ topspace X" using pathin_subtopology by (fastforce 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 \<subseteq> topspace X \<and>
(\<forall>x \<in> S. \<forall>y \<in> S. \<exists>g. pathin X g \<and> g \<in> {0..1} \<rightarrow> S \<and> g 0 = x \<and> 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 flip: image_subset_iff_funcset)
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) thenshow"connectedin X (g ` {0..1})" by (rule connectedin_continuous_map_image) auto qed auto show ?thesis using assms by (metis "*" connected_space_subconnected path_connected_space_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: "path_connected_space trivial_topology" 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" using pathin_const by (force simp: path_connectedin)
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" using continuous_map_def f by fastforce show ?thesis unfolding path_connectedin proof (intro conjI ballI; clarify?) fix x assume"x \ S" show"f x \ topspace Y" using S \<open>x \<in> S\<close> fX path_connectedin_subset_topspace by fastforce next fix x y assume"x \ S" and "y \ S" thenobtain 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\<open>pathin X g\<close> 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})" (is "?lhs = ?rhs") proof show"?lhs \ ?rhs" by (meson connectedin_discrete_topology path_connectedin_imp_connectedin) show"?rhs \ ?lhs" using subset_singletonD by fastforce qed
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: assumes"path_connected_space X" and"X homeomorphic_space Y" shows"path_connected_space Y" using assms homeomorphic_space_unfold path_connectedin_continuous_map_image by (metis homeomorphic_eq_everything_map path_connectedin_topspace)
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 show"subtopology Y (f ` U) homeomorphic_space subtopology X U" using assms unfolding homeomorphic_eq_everything_map by (metis Int_absorb1 assms(1) homeomorphic_map_subtopologies homeomorphic_space
homeomorphic_space_sym subset_image_inj inj_on_subset) 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\<open>Connected components\<close>
definition connected_component_of :: "'a topology \ 'a \ 'a \ bool" where"connected_component_of X x y \ \<exists>T. connectedin X T \<and> x \<in> T \<and> y \<in> 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\ \<Longrightarrow> 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\ \<Longrightarrow> connected_component_of (subtopology X T) x y" by (metis connected_component_of_def connectedin_subtopology inf.absorb_iff2 subtopology_subtopology)
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.31Bemerkung:
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
