Quelle Abstract_Topology_2.thy Sprache: Isabelle

(* 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"
 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 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)
 then show ?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 have to 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:
 "\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 \<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)"
 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>open V\<close> closure_closure inf_commute open_Int_closure_subset)
 then show "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 = {}"
 then have "openin (top_of_set S) (A \ V \ S)"
 by (simp add: inf_absorb2 openin_subtopology_Int)
 moreover have "A \ V \ S \ {}" using \x \ V\ \V \ A\ \x \ S\
 by auto
 ultimately show 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+
 then show ?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"
 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 \<open>compact S\<close> obtain D where "D \<subseteq> {T. open T \<and> S \<inter> T \<in> C}" and "finite D" and "S \<subseteq> \<Union>D"
 by (meson compactE)
 then have "image (\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 \
 (\<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"
 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 \<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
 then show "\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)"
 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>open T\<close> by (simp add: continuous_at_imp_continuous_on open_vimage)
 moreover have "y \ vimage f T"
 using \<open>x = f y\<close> \<open>x \<in> T\<close> by simp
 moreover have "vimage f T \ S"
 using \<open>T \<subseteq> image f S\<close> \<open>inj f\<close> unfolding inj_on_def subset_eq by auto
 ultimately have "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
 moreover have "closed (closure S \ f -` T)"
 using continuous_closed_preimage[OF contf] \<open>closed T\<close> 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

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

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>\<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)
 then show ?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
 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>\<open>tag unimportant\<close> \<open>Seperability\<close>

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 \: "\<And>T. openin(top_of_set S) T \<Longrightarrow> \<exists>\. \ \<subseteq> \ \<and> T = \<Union>\"
 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 \\<close> by blast
 show "\C. \C \ \ - {{}}\ \ openin (top_of_set S) C"
 by (simp add: \<open>\<And>C. C \<in> \ \<Longrightarrow> openin (top_of_set S) C\<close>)
 show "\\\\ - {{}}. T = \\" if "openin (top_of_set S) T" for T
 using \ [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)
 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 \<G> where "countable \<G> \<and> \<G> \<subseteq> tf ` \<F>" "\<Union>\<G> = \<Union>(tf ` \<F>)"
 using tf by (force intro: Lindelof [of "tf ` \"])
 then obtain \<F>' where \<F>': "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>"
 by (clarsimp simp add: countable_subset_image)
 then show ?thesis ..
qed

subsection\<^marker>\<open>tag unimportant\<close>\<open>Closed Maps\<close>

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>\<open>tag unimportant\<close>\<open>Open Maps\<close>

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>\<open>tag unimportant\<close>\<open>Quotient maps\<close>

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
 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
 \<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
 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 \<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
 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 (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)
 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"
 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
 then have "locally_finite_in X ((\i. T i \ f i -` U) ` I)"
 unfolding locally_finite_in_def
 using finite_subset [OF sub] fin by force
 then show "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)
 then show "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"
 then show "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"
 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"
 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)
 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
 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}"
 then show "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)
 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 \<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
 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)) \
 (\<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 ..
 then show ?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
 then show "r \ S \ S" "continuous_on S r"
 by auto
 then show "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
 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:
 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

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\<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
 then show ?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
 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 \<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
 then show "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)
 then show "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"
 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 \<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)

lemma connected_component_of_set:
--> --------------------

--> maximum size reached

--> --------------------

quality98%

¤ Dauer der Verarbeitung: 0.28 Sekunden (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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.