Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Sprache: Isabelle

Untersuchung 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
 "HOL-Library.Indicator_Function"
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)"
 apply auto
 apply (rule_tac x="d/2" in exI, auto)
 done

lemma triangle_lemma:
 fixes x y z :: real
 assumes x: "0 \ x"
 and y: "0 \ y"
 and z: "0 \ z"
 and xy: "x\<^sup>2 \ y\<^sup>2 + z\<^sup>2"
 shows "x \ y + z"
proof -
 have "y\<^sup>2 + z\<^sup>2 \ y\<^sup>2 + 2 * y * z + z\<^sup>2"
 using z y by simp
 with xy have th: "x\<^sup>2 \ (y + z)\<^sup>2"
 by (simp add: power2_eq_square field_simps)
 from y z have yz: "y + z \ 0"
 by arith
 from power2_le_imp_le[OF th yz] show ?thesis .
qed

lemma isCont_indicator:
 fixes x :: "'a::t2_space"
 shows "isCont (indicator A :: 'a \ real) x = (x \ frontier A)"
proof auto
 fix x
 assume cts_at: "isCont (indicator A :: 'a \ real) x" and fr: "x \ frontier A"
 with continuous_at_open have 1: "\V::real set. open V \ indicator A x \ V \
 (\<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
 hence "\U. open U \ x \ U \ (\y\U. indicator A y \ ({0<..<2} :: real set))"
 using 1 open_greaterThanLessThan by blast
 then guess U .. note U = this
 hence "\y\U. indicator A y > (0::real)"
 unfolding greaterThanLessThan_def by auto
 hence "U \ A" using indicator_eq_0_iff by force
 hence "x \ interior A" using U interiorI by auto
 thus ?thesis using fr unfolding frontier_def by simp
 next
 assume x: "x \ A"
 hence "indicator A x \ ({-1<..<1} :: real set)" by simp
 hence "\U. open U \ x \ U \ (\y\U. indicator A y \ ({-1<..<1} :: real set))"
 using 1 open_greaterThanLessThan by blast
 then guess U .. note U = this
 hence "\y\U. indicator A y < (1::real)"
 unfolding greaterThanLessThan_def by auto
 hence "U \ -A" by auto
 hence "x \ interior (-A)" using U interiorI by auto
 thus ?thesis using fr interior_complement unfolding frontier_def by auto
 qed
next
 assume nfr: "x \ frontier A"
 hence "x \ interior A \ x \ interior (-A)"
 by (auto simp: frontier_def closure_interior)
 thus "isCont ((indicator A)::'a \ real) x"
 proof
 assume int: "x \ interior A"
 then obtain U where U: "open U" "x \ U" "U \ A" unfolding interior_def by auto
 hence "\y\U. indicator A y = (1::real)" unfolding indicator_def by auto
 hence "continuous_on U (indicator A)" by (simp add: indicator_eq_1_iff)
 thus ?thesis using U continuous_on_eq_continuous_at by auto
 next
 assume ext: "x \ interior (-A)"
 then obtain U where U: "open U" "x \ U" "U \ -A" unfolding interior_def by auto
 then have "continuous_on U (indicator A)"
 using continuous_on_topological by (auto simp: subset_iff)
 thus ?thesis using U continuous_on_eq_continuous_at by auto
 qed
qed

lemma closedin_limpt:
 "closedin (top_of_set T) S \ S \ T \ (\x. x islimpt S \ x \ T \ x \ S)"
 apply (simp add: closedin_closed, safe)
 apply (simp add: closed_limpt islimpt_subset)
 apply (rule_tac x="closure S" in exI, simp)
 apply (force simp: closure_def)
 done

lemma closedin_closed_eq: "closed S \ closedin (top_of_set S) T \ closed T \ T \ S"
 by (meson closedin_limpt closed_subset closedin_closed_trans)

lemma connected_closed_set:
 "closed S
 \<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
 \<Longrightarrow> (closedin (top_of_set S) T \<longleftrightarrow>
 compact T \<and> T \<subseteq> 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)"
 proof (clarsimp simp: S)
 fix x
 assume "x \ closure (U \ V \ closure T)"
 then have "V \ closure T \ A \ x \ closure A" for A
 by (metis closure_mono subsetD inf.coboundedI2 inf_assoc)
 then have "x \ closure (T \ V)"
 by (metis \<open>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 (auto simp: openin_open intro!: exI[where x="V"])
 moreover have "A \ V \ S \ {}" using \x \ V\ \V \ A\ \x \ S\
 by auto
 ultimately have "T \ (A \ V \ S) \ {}"
 by (rule assms)
 with \<open>T \<inter> A = {}\<close> show False by auto
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:
 "\connected s; s \ t \ {}; s - t \ {}\ \ (s \ frontier t \ {})"
 apply (simp add: frontier_interiors connected_openin, safe)
 apply (drule_tac x="s \ interior t" in spec, safe)
 apply (drule_tac [2] x="s \ interior (-t)" in spec)
 apply (auto simp: disjoint_eq_subset_Compl dest: interior_subset [THEN subsetD])
 done

subsection \<open>Compactness\<close>

lemma openin_delete:
 fixes a :: "'a :: t1_space"
 shows "openin (top_of_set u) s
 \<Longrightarrow> 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"
 apply (rule subset_trans)
 by (metis Int_Union Int_lower2 \<open>D \<subseteq> (\<inter>) S ` C\<close> image_inv_into_cancel)
 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
 unfolding subset_eq
 by auto

lemma image_closure_subset:
 assumes contf: "continuous_on (closure S) f"
 and "closed T"
 and "(f ` S) \ T"
 shows "f ` (closure S) \ T"
proof -
 have "S \ {x \ closure S. f x \ T}"
 using assms(3) closure_subset by auto
 moreover have "closed (closure S \ f -` T)"
 using continuous_closed_preimage[OF contf] \<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

subsection\<^marker>\<open>tag unimportant\<close> \<open>A function constant on a set\<close>

definition constant_on (infixl "(constant'_on)" 50)
 where "f constant_on A \ \y. \x\A. f x = y"

lemma constant_on_subset: "\f constant_on A; B \ A\ \ f constant_on B"
 unfolding constant_on_def by blast

lemma injective_not_constant:
 fixes S :: "'a::{perfect_space} set"
 shows "\open S; inj_on f S; f constant_on S\ \ S = {}"
unfolding constant_on_def
by (metis equals0I inj_on_contraD islimpt_UNIV islimpt_def)

lemma constant_on_closureI:
 fixes f :: "_ \ 'b::t1_space"
 assumes cof: "f constant_on S" and contf: "continuous_on (closure S) f"
 shows "f constant_on (closure S)"
using continuous_constant_on_closure [OF contf] cof unfolding constant_on_def
by metis

subsection\<^marker>\<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_union Un_iff trivial_limit_within)

lemma continuous_on_cases_local:
 "\closedin (top_of_set (s \ t)) s; closedin (top_of_set (s \ t)) t;
 continuous_on s f; continuous_on t g;
 \<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 {t \ s. h t \ a} f"
 and "continuous_on {t \ s. a \ h t} g"
 and h: "continuous_on s h"
 and "\t. \t \ s; h t = a\ \ f t = g t"
 shows "continuous_on s (\t. if h t \ a then f(t) else g(t))"
proof -
 have s: "s = (s \ h -` atMost a) \ (s \ h -` atLeast a)"
 by force
 have 1: "closedin (top_of_set s) (s \ h -` atMost a)"
 by (rule continuous_closedin_preimage [OF h closed_atMost])
 have 2: "closedin (top_of_set s) (s \ h -` atLeast a)"
 by (rule continuous_closedin_preimage [OF h closed_atLeast])
 have eq: "s \ h -` {..a} = {t \ s. h t \ a}" "s \ h -` {a..} = {t \ s. a \ h t}"
 by auto
 show ?thesis
 apply (rule continuous_on_subset [of s, OF _ order_refl])
 apply (subst s)
 apply (rule continuous_on_cases_local)
 using 1 2 s assms apply (auto simp: eq)
 done
qed

lemma continuous_on_cases_1:
 fixes s :: "real set"
 assumes "continuous_on {t \ s. t \ a} f"
 and "continuous_on {t \ s. a \ t} g"
 and "a \ s \ f a = g a"
 shows "continuous_on s (\t. if t \ a then f(t) else g(t))"
using assms
by (auto intro: continuous_on_cases_le [where h = id, simplified])

subsection\<^marker>\<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]
 apply clarify
 apply (rule_tac x="\ - {{}}" in exI, auto)
 done
 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 (meson img openin_Int openin_subtopology_Int_subset openin_subtopology_self)
 show ?rhs
 using g [OF *] eq by auto
 next
 assume rhs: ?rhs
 show ?lhs
 by (metis f fg image_eqI image_subset_iff imf img openin_subopen openin_subtopology_self openin_trans rhs)
 qed
qed

lemma continuous_left_inverse_imp_quotient_map:
 assumes "continuous_on S f"
 and "continuous_on (f ` S) g"
 and "\x. x \ S \ g(f x) = x"
 and "U \ f ` S"
 shows "openin (top_of_set S) (S \ f -` U) \
 openin (top_of_set (f ` S)) U"
apply (rule continuous_right_inverse_imp_quotient_map)
using assms apply force+
done

lemma continuous_imp_quotient_map:
 fixes f :: "'a::t2_space \ 'b::t2_space"
 assumes "continuous_on S f" "f ` S = T" "compact S" "U \ T"
 shows "openin (top_of_set S) (S \ f -` U) \
 openin (top_of_set T) U"
 by (metis (no_types, lifting) assms closed_map_imp_quotient_map continuous_imp_closed_map)

subsection\<^marker>\<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"
 show "continuous_map X Y ?h"
 apply (rule pasting_lemma [OF ope cont])
 apply (blast intro: f)+
 by (metis (no_types, lifting) UN_E X subsetD someI_ex)
 show "f (SOME i. i \ I \ x \ T i) x = f i x" if "i \ I" "x \ topspace X \ T i" for i x
 by (metis (no_types, lifting) IntD2 IntI f someI_ex that)
qed

lemma pasting_lemma_locally_finite:
 assumes fin: "\x. x \ topspace X \ \V. openin X V \ x \ V \ finite {i \ I. T i \ V \ {}}"
 and clo: "\i. i \ I \ closedin X (T i)"
 and cont: "\i. i \ I \ continuous_map(subtopology X (T i)) Y (f i)"
 and f: "\i j x. \i \ I; j \ I; x \ topspace X \ T i \ T j\ \ f i x = f j x"
 and g: "\x. x \ topspace X \ \j. j \ I \ x \ T j \ g x = f j x"
 shows "continuous_map X Y g"
 unfolding continuous_map_closedin_preimage_eq
proof (intro conjI allI impI)
 show "g ` topspace X \ topspace Y"
 using g cont continuous_map_image_subset_topspace by fastforce
next
 fix U
 assume Y: "closedin Y U"
 have T: "T i \ topspace X" if "i \ I" for i
 using clo by (simp add: closedin_subset that)
 have *: "topspace X \ g -` U = (\i \ I. T i \ f i -` U)"
 using f g T by fastforce
 have cTf: "\i. i \ I \ closedin X (T i \ f i -` U)"
 using cont unfolding continuous_map_closedin_preimage_eq topspace_subtopology
 by (simp add: Int_absorb1 T Y clo closedin_closed_subtopology)
 have sub: "{Z \ (\i. T i \ f i -` U) ` I. Z \ V \ {}}
 \<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 lf: "locally_finite_in X ((\i. T i \ f i -` U) ` I)"
 unfolding locally_finite_in_def
 using finite_subset [OF sub] fin by force
 show "closedin X (topspace X \ g -` U)"
 apply (subst *)
 apply (rule closedin_locally_finite_Union)
 apply (auto intro: cTf lf)
 done
qed

subsubsection\<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
 show "continuous_map X Y (\x. f(@i. i \ I \ x \ T i) x)"
 apply (rule pasting_lemma_locally_finite [OF fin])
 apply (blast intro: assms)+
 by (metis (no_types, lifting) UN_E X set_rev_mp someI_ex)
next
 fix x i
 assume "i \ I" and "x \ topspace X \ T i"
 show "f (SOME i. i \ I \ x \ T i) x = f i x"
 apply (rule someI2_ex)
 using \<open>i \<in> I\<close> \<open>x \<in> topspace X \<inter> T i\<close> apply blast
 by (meson Int_iff \<open>i \<in> I\<close> \<open>x \<in> topspace X \<inter> T i\<close> f)
qed

lemma pasting_lemma_exists_closed:
 assumes fin: "finite I"
 and X: "topspace X \ \(T ` I)"
 and clo: "\i. i \ I \ closedin X (T i)"
 and cont: "\i. i \ I \ continuous_map(subtopology X (T i)) Y (f i)"
 and f: "\i j x. \i \ I; j \ I; x \ topspace X \ T i \ T j\ \ f i x = f j x"
 obtains g where "continuous_map X Y g" "\x i. \i \ I; x \ topspace X \ T i\ \ g x = f i x"
proof
 show "continuous_map X Y (\x. f (SOME i. i \ I \ x \ T i) x)"
 apply (rule pasting_lemma_closed [OF \<open>finite I\<close> clo cont])
 apply (blast intro: f)+
 by (metis (mono_tags, lifting) UN_iff X someI_ex subset_iff)
next
 fix x i
 assume "i \ I" "x \ topspace X \ T i"
 then show "f (SOME i. i \ I \ x \ T i) x = f i x"
 by (metis (no_types, lifting) IntD2 IntI f someI_ex)
qed

lemma continuous_map_cases:
 assumes f: "continuous_map (subtopology X (X closure_of {x. P x})) Y f"
 and g: "continuous_map (subtopology X (X closure_of {x. \ P x})) Y g"
 and fg: "\x. x \ X frontier_of {x. P x} \ f x = g x"
 shows "continuous_map X Y (\x. if P x then f x else g x)"
proof (rule pasting_lemma_closed)
 let ?f = "\b. if b then f else g"
 let ?g = "\x. if P x then f x else g x"
 let ?T = "\b. if b then X closure_of {x. P x} else X closure_of {x. ~P x}"
 show "finite {True,False}" by auto
 have eq: "topspace X - Collect P = topspace X \ {x. \ P x}"
 by blast
 show "?f i x = ?f j x"
 if "i \ {True,False}" "j \ {True,False}" and x: "x \ topspace X \ ?T i \ ?T j" for i j x
 proof -
 have "f x = g x"
 if "i" "\ j"
 apply (rule fg)
 unfolding frontier_of_closures eq
 using x that closure_of_restrict by fastforce
 moreover
 have "g x = f x"
 if "x \ X closure_of {x. \ P x}" "x \ X closure_of Collect P" "\ i" "j" for x
 apply (rule fg [symmetric])
 unfolding frontier_of_closures eq
 using x that closure_of_restrict by fastforce
 ultimately show ?thesis
 using that by (auto simp flip: closure_of_restrict)
 qed
 show "\j. j \ {True,False} \ x \ ?T j \ (if P x then f x else g x) = ?f j x"
 if "x \ topspace X" for x
 apply simp
 apply safe
 apply (metis Int_iff closure_of inf_sup_absorb mem_Collect_eq that)
 by (metis DiffI eq closure_of_subset_Int contra_subsetD mem_Collect_eq that)
qed (auto simp: f g)

lemma continuous_map_cases_alt:
 assumes f: "continuous_map (subtopology X (X closure_of {x \ topspace X. P x})) Y f"
 and g: "continuous_map (subtopology X (X closure_of {x \ topspace X. ~P x})) Y g"
 and fg: "\x. x \ X frontier_of {x \ topspace X. P x} \ f x = g x"
 shows "continuous_map X Y (\x. if P x then f x else g x)"
 apply (rule continuous_map_cases)
 using assms
 apply (simp_all add: Collect_conj_eq closure_of_restrict [symmetric] frontier_of_restrict [symmetric])
 done

lemma continuous_map_cases_function:
 assumes contp: "continuous_map X Z p"
 and contf: "continuous_map (subtopology X {x \ topspace X. p x \ Z closure_of U}) Y f"
 and contg: "continuous_map (subtopology X {x \ topspace X. p x \ Z closure_of (topspace Z - U)}) Y g"
 and fg: "\x. \x \ topspace X; p x \ Z frontier_of U\ \ f x = g x"
 shows "continuous_map X Y (\x. if p x \ U then f x else g x)"
proof (rule continuous_map_cases_alt)
 show "continuous_map (subtopology X (X closure_of {x \ topspace X. p x \ U})) Y f"
 proof (rule continuous_map_from_subtopology_mono)
 let ?T = "{x \ topspace X. p x \ Z closure_of U}"
 show "continuous_map (subtopology X ?T) Y f"
 by (simp add: contf)
 show "X closure_of {x \ topspace X. p x \ U} \ ?T"
 by (rule continuous_map_closure_preimage_subset [OF contp])
 qed
 show "continuous_map (subtopology X (X closure_of {x \ topspace X. p x \ U})) Y g"
 proof (rule continuous_map_from_subtopology_mono)
 let ?T = "{x \ topspace X. p x \ Z closure_of (topspace Z - U)}"
 show "continuous_map (subtopology X ?T) Y g"
 by (simp add: contg)
 have "X closure_of {x \ topspace X. p x \ U} \ X closure_of {x \ topspace X. p x \ topspace Z - U}"
 apply (rule closure_of_mono)
 using continuous_map_closedin contp by fastforce
 then show "X closure_of {x \ topspace X. p x \ U} \ ?T"
 by (rule order_trans [OF _ continuous_map_closure_preimage_subset [OF contp]])
 qed
next
 show "f x = g x" if "x \ X frontier_of {x \ topspace X. p x \ U}" for x
 using that continuous_map_frontier_frontier_preimage_subset [OF contp, of U] fg by blast
qed

subsection \<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 ` S \<subseteq> T \<and> (\<forall>x\<in>T. r x = x)"

definition\<^marker>\<open>tag important\<close> retract_of (infixl "retract'_of" 50) where
"T retract_of S \ (\r. retraction S T r)"

lemma retraction_idempotent: "retraction S T r \ x \ S \ r (r x) = r x"
 unfolding retraction_def by auto

text \<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 (meson contt contr assms(4) contg assms(8) continuous_on_compose continuous_on_subset)
 show "(i \ g \ r) ` S \ S"
 using assms(2,4,8) by force
 qed
 then obtain x where x: "x \ S" "(i \ g \ r) x = x" ..
 then have *: "g (r x) \ T"
 using assms(4,8) by auto
 have "r ((i \ g \ r) x) = r x"
 using x by auto
 then show ?thesis
 using "*" ri that by auto
qed

lemma homeomorphic_fixpoint_property:
 fixes S :: "'a::topological_space set"
 and T :: "'b::topological_space set"
 assumes "S homeomorphic T"
 shows "(\f. continuous_on S f \ f ` S \ S \ (\x\S. f x = x)) \
 (\<forall>g. continuous_on T g \<and> g ` T \<subseteq> 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 show ?rhs
 by (metis invertible_fixpoint_property[of T i S r] order_refl)
 next
 assume ?rhs
 with r show ?lhs
 by (metis invertible_fixpoint_property[of S r T i] order_refl)
 qed
qed

lemma retract_fixpoint_property:
 fixes f :: "'a::topological_space \ 'b::topological_space"
 and S :: "'a set"
 assumes "T retract_of S"
 and FP: "\f. \continuous_on S f; f ` S \ S\ \ \x\S. f x = x"
 and contg: "continuous_on T g"
 and "g ` T \ T"
 obtains y where "y \ T" and "g y = y"
proof -
 obtain h where "retraction S T h"
 using assms(1) unfolding retract_of_def ..
 then show ?thesis
 unfolding retraction_def
 using invertible_fixpoint_property[OF continuous_on_id _ _ _ _ FP]
 by (metis assms(4) contg image_ident that)
qed

lemma retraction:
 "retraction S T r \
 T \<subseteq> S \<and> continuous_on S r \<and> r ` S = T \<and> (\<forall>x \<in> T. r x = x)"
 by (force simp: retraction_def)

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 "T = r ` S" "r ` S \ S" "continuous_on S r"
 by simp_all
 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 "retraction T S r"
 by (auto simp add: retract_of_def)
 show thesis
 by (rule that [of "f \ r"])
 (use \<open>continuous_on S f\<close> \<open>f ` S \<subseteq> U\<close> \<open>retraction T S r\<close> in \<open>auto simp: continuous_on_compose2 retraction\<close>)
qed

lemma idempotent_imp_retraction:
 assumes "continuous_on S f" and "f ` S \ S" and "\x. x \ S \ f(f x) = f x"
 shows "retraction S (f ` S) f"
by (simp add: assms retraction)

lemma retraction_subset:
 assumes "retraction S T r" and "T \ s'" and "s' \ S"
 shows "retraction s' T r"
 unfolding retraction_def
 by (metis assms continuous_on_subset image_mono retraction)

lemma retract_of_subset:
 assumes "T retract_of S" and "T \ s'" and "s' \ S"
 shows "T retract_of s'"
by (meson assms retract_of_def retraction_subset)

lemma retraction_refl [simp]: "retraction S S (\x. x)"
by (simp add: retraction)

lemma retract_of_refl [iff]: "S retract_of S"
 unfolding retract_of_def retraction_def
 using continuous_on_id by blast

lemma retract_of_imp_subset:
 "S retract_of T \ S \ T"
by (simp add: retract_of_def retraction_def)

lemma retract_of_empty [simp]:
 "({} retract_of S) \ S = {}" "(S retract_of {}) \ S = {}"
by (auto simp: retract_of_def retraction_def)

lemma retract_of_singleton [iff]: "({x} retract_of S) \ x \ S"
 unfolding retract_of_def retraction_def by force

lemma retraction_comp:
 "\retraction S T f; retraction T U g\
 \<Longrightarrow> retraction S U (g \<circ> f)"
apply (auto simp: retraction_def intro: continuous_on_compose2)
by blast

lemma retract_of_trans [trans]:
 assumes "S retract_of T" and "T retract_of U"
 shows "S retract_of U"
using assms by (auto simp: retract_of_def intro: retraction_comp)

lemma closedin_retract:
 fixes S :: "'a :: t2_space set"
 assumes "S retract_of T"
 shows "closedin (top_of_set T) S"
proof -
 obtain r where r: "S \ T" "continuous_on T r" "r ` T \ S" "\x. x \ S \ r x = x"
 using assms by (auto simp: retract_of_def retraction_def)
 have "S = {x\T. x = r x}"
 using r by auto
 also have "\ = T \ ((\x. (x, r x)) -` ({y. \x. y = (x, x)}))"
 unfolding vimage_def mem_Times_iff fst_conv snd_conv
 using r
 by auto
 also have "closedin (top_of_set T) \"
 by (rule continuous_closedin_preimage) (auto intro!: closed_diagonal continuous_on_Pair r)
 finally show ?thesis .
qed

lemma closedin_self [simp]: "closedin (top_of_set S) S"
 by simp

lemma retract_of_closed:
 fixes S :: "'a :: t2_space set"
 shows "\closed T; S retract_of T\ \ closed S"
 by (metis closedin_retract closedin_closed_eq)

lemma retract_of_compact:
 "\compact T; S retract_of T\ \ compact S"
 by (metis compact_continuous_image retract_of_def retraction)

lemma retract_of_connected:
 "\connected T; S retract_of T\ \ connected S"
 by (metis Topological_Spaces.connected_continuous_image retract_of_def retraction)

lemma retraction_openin_vimage_iff:
 "openin (top_of_set S) (S \ r -` U) \ openin (top_of_set T) U"
 if retraction: "retraction S T r" and "U \ T"
 using retraction apply (rule retractionE)
 apply (rule continuous_right_inverse_imp_quotient_map [where g=r])
 using \<open>U \<subseteq> T\<close> apply (auto elim: continuous_on_subset)
 done

lemma retract_of_Times:
 "\S retract_of s'; T retract_of t'\ \ (S \ T) retract_of (s' \ t')"
apply (simp add: retract_of_def retraction_def Sigma_mono, clarify)
apply (rename_tac f g)
apply (rule_tac x="\z. ((f \ fst) z, (g \ snd) z)" in exI)
apply (rule conjI continuous_intros | erule continuous_on_subset | force)+
done

subsection\<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 \ topspace X = {}"
 by (auto simp: continuous_map_def retract_of_space_def)

lemma retract_of_space_singleton [simp]:
 "{a} retract_of_space X \ a \ topspace X"
proof -
 have "continuous_map X (subtopology X {a}) (\x. a) \ (\x. a) a = a" if "a \ topspace X"
 using that by simp
 then show ?thesis
 by (force simp: retract_of_space_def)
qed

lemma retract_of_space_clopen:
 assumes "openin X S" "closedin X S" "S = {} \ topspace X = {}"
 shows "S retract_of_space X"
proof (cases "S = {}")
 case False
 then obtain a where "a \ S"
 by blast
 show ?thesis
 unfolding retract_of_space_def
 proof (intro exI conjI)
 show "S \ topspace X"
 by (simp add: assms closedin_subset)
 have "continuous_map X X (\x. if x \ S then x else a)"
 proof (rule continuous_map_cases)
 show "continuous_map (subtopology X (X closure_of {x. x \ S})) X (\x. x)"
 by (simp add: continuous_map_from_subtopology)
 show "continuous_map (subtopology X (X closure_of {x. x \ S})) X (\x. a)"
 using \<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 = {} \ topspace X = {}"
 shows "S retract_of_space X"
proof (rule retract_of_space_clopen)
 have "S \ T = {}"
 by (meson ST disjnt_def)
 then have "S = topspace X - T"
 using ST by auto
 then show "closedin X S"
 using \<open>openin X T\<close> by blast
qed (auto simp: assms)

lemma retraction_maps_section_image1:
 assumes "retraction_maps X Y r s"
 shows "s ` (topspace Y) retract_of_space X"
 unfolding retract_of_space_section_map
proof
 show "s ` topspace Y \ topspace X"
 using assms continuous_map_image_subset_topspace retraction_maps_def by blast
 show "section_map (subtopology X (s ` topspace Y)) X id"
 unfolding section_map_def
 using assms retraction_maps_to_retract_maps by blast
qed

lemma retraction_maps_section_image2:
 "retraction_maps X Y r s
 \<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

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:
 "pathin X (\x. a) \ a \ topspace X"
 by (simp add: pathin_def)

lemma path_start_in_topspace: "pathin X g \ g 0 \ topspace X"
 by (force simp: pathin_def continuous_map)

lemma path_finish_in_topspace: "pathin X g \ g 1 \ topspace X"
 by (force simp: pathin_def continuous_map)

lemma path_image_subset_topspace: "pathin X g \ g ` ({0..1}) \ topspace X"
 by (force simp: pathin_def continuous_map)

definition path_connected_space :: "'a topology \ bool"
 where "path_connected_space X \ \x \ topspace X. \ y \ topspace X. \g. pathin X g \ g 0 = x \ g 1 = y"

definition path_connectedin :: "'a topology \ 'a set \ bool"
 where "path_connectedin X S \ S \ topspace X \ path_connected_space(subtopology X S)"

lemma path_connectedin_absolute [simp]:
 "path_connectedin (subtopology X S) S \ path_connectedin X S"
 by (simp add: path_connectedin_def subtopology_subtopology)

lemma path_connectedin_subset_topspace:
 "path_connectedin X S \ S \ topspace X"
 by (simp add: path_connectedin_def)

lemma path_connectedin_subtopology:
 "path_connectedin (subtopology X S) T \ path_connectedin X T \ T \ S"
 by (auto simp: path_connectedin_def subtopology_subtopology inf.absorb2)

lemma path_connectedin:
 "path_connectedin X S \
 S \<subseteq> topspace X \<and>
 (\<forall>x \<in> S. \<forall>y \<in> S. \<exists>g. pathin X g \<and> g ` {0..1} \<subseteq> 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)

lemma path_connectedin_topspace:
 "path_connectedin X (topspace X) \ path_connected_space X"
 by (simp add: path_connectedin_def)

lemma path_connected_imp_connected_space:
 assumes "path_connected_space X"
 shows "connected_space X"
proof -
 have *: "\S. connectedin X S \ g 0 \ S \ g 1 \ S" if "pathin X g" for g
 proof (intro exI conjI)
 have "continuous_map (subtopology euclideanreal {0..1}) X g"
 using connectedin_absolute that by (simp add: pathin_def)
 then show "connectedin X (g ` {0..1})"
 by (rule connectedin_continuous_map_image) auto
 qed auto
 show ?thesis
 using assms
 by (auto intro: * simp add: path_connected_space_def connected_space_subconnected Ball_def)
qed

lemma path_connectedin_imp_connectedin:
 "path_connectedin X S \ connectedin X S"
 by (simp add: connectedin_def path_connected_imp_connected_space path_connectedin_def)

lemma path_connected_space_topspace_empty:
 "topspace X = {} \ path_connected_space X"
 by (simp add: path_connected_space_def)

lemma path_connectedin_empty [simp]: "path_connectedin X {}"
 by (simp add: path_connectedin)

lemma path_connectedin_singleton [simp]: "path_connectedin X {a} \ a \ topspace X"
proof
 show "path_connectedin X {a} \ a \ topspace X"
 by (simp add: path_connectedin)
 show "a \ topspace X \ path_connectedin X {a}"
 unfolding path_connectedin
 using pathin_const by fastforce
qed

lemma path_connectedin_continuous_map_image:
 assumes f: "continuous_map X Y f" and S: "path_connectedin X S"
 shows "path_connectedin Y (f ` S)"
proof -
 have fX: "f ` (topspace X) \ topspace Y"
 by (metis f continuous_map_image_subset_topspace)
 show ?thesis
 unfolding path_connectedin
 proof (intro conjI ballI; clarify?)
 fix x
 assume "x \ S"
 show "f x \ topspace Y"
 by (meson S fX \<open>x \<in> S\<close> image_subset_iff path_connectedin_subset_topspace set_mp)
 next
 fix x y
 assume "x \ S" and "y \ S"
 then obtain g where g: "pathin X g" "g ` {0..1} \ S" "g 0 = x" "g 1 = y"
 using S by (force simp: path_connectedin)
 show "\g. pathin Y g \ g ` {0..1} \ f ` S \ g 0 = f x \ g 1 = f y"
 proof (intro exI conjI)
 show "pathin Y (f \ g)"
 using \<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})"
 apply safe
 using path_connectedin_subset_topspace apply fastforce
 apply (meson connectedin_discrete_topology path_connectedin_imp_connectedin)
 using subset_singletonD by fastforce

lemma path_connected_space_discrete_topology:
 "path_connected_space (discrete_topology U) \ (\a. U \ {a})"
 by (metis path_connectedin_discrete_topology path_connectedin_topspace path_connected_space_topspace_empty
 subset_singletonD topspace_discrete_topology)

lemma homeomorphic_path_connected_space_imp:
 "\path_connected_space X; X homeomorphic_space Y\ \ path_connected_space Y"
 unfolding homeomorphic_space_def homeomorphic_maps_def
 by (metis (no_types, hide_lams) continuous_map_closedin continuous_map_image_subset_topspace imageI order_class.order.antisym path_connectedin_continuous_map_image path_connectedin_topspace subsetI)

lemma homeomorphic_path_connected_space:
 "X homeomorphic_space Y \ path_connected_space X \ path_connected_space Y"
 by (meson homeomorphic_path_connected_space_imp homeomorphic_space_sym)

lemma homeomorphic_map_path_connectedness:
 assumes "homeomorphic_map X Y f" "U \ topspace X"
 shows "path_connectedin Y (f ` U) \ path_connectedin X U"
 unfolding path_connectedin_def
proof (intro conj_cong homeomorphic_path_connected_space)
 show "(f ` U \ topspace Y) = (U \ topspace X)"
 using assms homeomorphic_imp_surjective_map by blast
next
 assume "U \ topspace X"
 show "subtopology Y (f ` U) homeomorphic_space subtopology X U"
 using assms unfolding homeomorphic_eq_everything_map
 by (metis (no_types, hide_lams) assms homeomorphic_map_subtopologies homeomorphic_space homeomorphic_space_sym image_mono inf.absorb_iff2)
qed

lemma homeomorphic_map_path_connectedness_eq:
 "homeomorphic_map X Y f \ path_connectedin X U \ U \ topspace X \ path_connectedin Y (f ` U)"
 by (meson homeomorphic_map_path_connectedness path_connectedin_def)

subsection\<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:
 "connected_component_of_set X x = {y. \T. connectedin X T \ x \ T \ y \ T}"
 by (meson connected_component_of_def)

lemma connected_component_of_subset_topspace:
 "connected_component_of_set X x \ topspace X"
 using connected_component_in_topspace by force

lemma connected_component_of_eq_empty:
 "connected_component_of_set X x = {} \ (x \ topspace X)"
 using connected_component_in_topspace connected_component_of_refl by fastforce

lemma connected_space_iff_connected_component:
 "connected_space X \ (\x \ topspace X. \y \ topspace X. connected_component_of X x y)"
 by (simp add: connected_component_of_def connected_space_subconnected)

lemma connected_space_imp_connected_component_of:
 "\connected_space X; a \ topspace X; b \ topspace X\
 \<Longrightarrow> connected_component_of X a b"
 by (simp add: connected_space_iff_connected_component)

lemma connected_space_connected_component_set:
 "connected_space X \ (\x \ topspace X. connected_component_of_set X x = topspace X)"
 using connected_component_of_subset_topspace connected_space_iff_connected_component by fastforce

lemma connected_component_of_maximal:
 "\connectedin X S; x \ S\ \ S \ connected_component_of_set X x"
 by (meson Ball_Collect connected_component_of_def)

lemma connected_component_of_equiv:
 "connected_component_of X x y \
 x \<in> topspace X \<and> y \<in> topspace X \<and> connected_component_of X x = connected_component_of X y"
 apply (simp add: connected_component_in_topspace fun_eq_iff)
 by (meson connected_component_of_refl connected_component_of_sym connected_component_of_trans)

lemma connected_component_of_disjoint:
 "disjnt (connected_component_of_set X x) (connected_component_of_set X y)
 \<longleftrightarrow> ~(connected_component_of X x y)"
 using connected_component_of_equiv unfolding disjnt_iff by force

lemma connected_component_of_eq:
 "connected_component_of X x = connected_component_of X y \
 (x \<notin> topspace X) \<and> (y \<notin> topspace X) \<or>
 x \<in> topspace X \<and> y \<in> topspace X \<and>
 connected_component_of X x y"
 by (metis Collect_empty_eq_bot connected_component_of_eq_empty connected_component_of_equiv)

lemma connectedin_connected_component_of:
 "connectedin X (connected_component_of_set X x)"
proof -
 have "connected_component_of_set X x = \ {T. connectedin X T \ x \ T}"
--> --------------------

--> maximum size reached

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

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.106Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

Druckansicht unsichere Verbindung
Druckansicht Hier finden Sie eine Liste der Produkte des Unternehmens
Mittel

Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Sprache: Isabelle

Untersuchung Isabelle^©

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.106Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

schauen Sie vor die Tür

Die Firma ist wie angegeben erreichbar.

Bot Zugriff

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Sprache: Isabelle

Untersuchung Isabelle©

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.106Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

schauen Sie vor die Tür

Die Firma ist wie angegeben erreichbar.

Bot Zugriff

^© Kompilation durch diese Firma

Untersuchung Isabelle^©