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 ‹Abstract Topology 2›

theory Abstract_Topology_2
  imports
    Elementary_Topology Abstract_Topology Continuum_Not_Denumerable
    "HOL-Library.Indicator_Function"
    "HOL-Library.Equipollence"
begin

text ‹Combination of Elementary and Abstract Topology›

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 \
    (∃U::'a set. open U \ x \ U \ (\y\U. indicator A y \ V))" by auto
  show False
  proof (cases "x \ A")
    assume x: "x \ A"
    hence "indicator A x \ ({0<..<2} :: real set)" by simp
    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
    ==> connected S ⟷ (∄A B. closed A ∧ closed B ∧ A ≠ {} ∧ B ≠ {} ∧ A ∪ B = S ∧ A ∩ B = {})"
  unfolding connected_closedin_eq closedin_closed_eq connected_closedin_eq by blast

text ‹If a connnected set is written as the union of two nonempty closed sets, 
  then these sets have to intersect.›

lemma connected_as_closed_union:
  assumes "connected C" "C = A \ B" "closed A" "closed B" "A \ {}" "B \ {}"
  shows "A \ B \ {}"
  by (metis assms closed_Un connected_closed_set)

lemma closedin_subset_trans:
  "closedin (top_of_set U) S \ S \ T \ T \ U \
    closedin (top_of_set T) S"
  by (meson closedin_limpt subset_iff)

lemma openin_subset_trans:
  "openin (top_of_set U) S \ S \ T \ T \ U \
    openin (top_of_set T) S"
  by (auto simp: openin_open)

lemma closedin_compact:
  "\compact S; closedin (top_of_set S) T\ \ compact T"
  by (metis closedin_closed compact_Int_closed)

lemma closedin_compact_eq:
  fixes S :: "'a::t2_space set"
  shows "compact S \ (closedin (top_of_set S) T \ compact T \ T \ S)"
  by (metis closedin_imp_subset closedin_compact closed_subset compact_imp_closed)


subsection ‹Closure›

lemma euclidean_closure_of [simp]: "euclidean closure_of S = closure S"
  by (auto simp: closure_of_def closure_def islimpt_def)

lemma closure_openin_Int_closure:
  assumes ope: "openin (top_of_set U) S" and "T \ U"
  shows "closure(S \ closure T) = closure(S \ T)"
proof
  obtain V where "open V" and S: "S = U \ V"
    using ope using openin_open by metis
  show "closure (S \ closure T) \ closure (S \ T)"
    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 V› closure_closure inf_commute open_Int_closure_subset)
      then show "x \ closure (U \ V \ T)"
        by (metis ‹T ⊆ U› inf.absorb_iff2 inf_assoc inf_commute)
    qed
next
  show "closure (S \ T) \ closure (S \ closure T)"
    by (meson Int_mono closure_mono closure_subset order_refl)
qed

corollary infinite_openin:
  fixes S :: "'a :: t1_space set"
  shows "\openin (top_of_set U) S; x \ S; x islimpt U\ \ infinite S"
  by (clarsimp simp add: openin_open islimpt_eq_acc_point inf_commute)

lemma closure_Int_ballI:
  assumes "\U. \openin (top_of_set S) U; U \ {}\ \ T \ U \ {}"
  shows "S \ closure T"
proof (clarsimp simp: closure_iff_nhds_not_empty)
  fix x and A and V
  assume "x \ S" "V \ A" "open V" "x \ V" "T \ A = {}"
  then have "openin (top_of_set S) (A \ V \ S)"
    by (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 ‹T ∩ A = {}› assms by fastforce
qed


subsection ‹Frontier›

lemma euclidean_interior_of [simp]: "euclidean interior_of S = interior S"
  by (auto simp: interior_of_def interior_def)

lemma euclidean_frontier_of [simp]: "euclidean frontier_of S = frontier S"
  by (auto simp: frontier_of_def frontier_def)

lemma connected_Int_frontier:
  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 ‹connected S› [unfolded connected_openin]
    by (metis assms connectedin_Int_frontier_of connectedin_iff_connected euclidean_frontier_of)
qed

subsection ‹Compactness›

lemma openin_delete:
  fixes a :: "'a :: t1_space"
  shows "openin (top_of_set u) S \ openin (top_of_set u) (S - {a})"
by (metis Int_Diff open_delete openin_open)

lemma compact_eq_openin_cover:
  "compact S \
    (∀C. (∀c∈C. openin (top_of_set S) c) ∧ S ⊆ ∪C ⟶
      (∃D⊆C. finite D ∧ S ⊆ ∪D))"
proof safe
  fix C
  assume "compact S" and "\c\C. openin (top_of_set S) c" and "S \ \C"
  then have "\c\{T. open T \ S \ T \ C}. open c" and "S \ \{T. open T \ S \ T \ C}"
    unfolding openin_open by force+
  with ‹compact S› obtain D where "D \ {T. open T \ S \ T \ C}" and "finite D" and "S \ \D"
    by (meson compactE)
  then have "image (\T. S \ T) D \ C \ finite (image (\T. S \ T) D) \ S \ \(image (\T. S \ T) D)"
    by auto
  then show "\D\C. finite D \ S \ \D" ..
next
  assume 1: "\C. (\c\C. openin (top_of_set S) c) \ S \ \C \
        (∃D⊆C. finite D ∧ S ⊆ ∪D)"
  show "compact S"
  proof (rule compactI)
    fix C
    let ?C = "image (\T. S \ T) C"
    assume "\t\C. open t" and "S \ \C"
    then have "(\c\?C. openin (top_of_set S) c) \ S \ \?C"
      unfolding openin_open by auto
    with 1 obtain D where "D \ ?C" and "finite D" and "S \ \D"
      by metis
    let ?D = "inv_into C (\T. S \ T) ` D"
    have "?D \ C \ finite ?D \ S \ \?D"
    proof (intro conjI)
      from ‹D ⊆ ?C› show "?D \ C"
        by (fast intro: inv_into_into)
      from ‹finite D› show "finite ?D"
        by (rule finite_imageI)
      from ‹S ⊆ ∪D› show "S \ \?D"
        by (metis ‹D ⊆ (∩) S ` C› image_inv_into_cancel inf_Sup le_infE)
    qed
    then show "\D\C. finite D \ S \ \D" ..
  qed
qed


subsection ‹Continuity›

lemma interior_image_subset:
  assumes "inj f" "\x. continuous (at x) f"
  shows "interior (f ` S) \ f ` (interior S)"
proof
  fix x assume "x \ interior (f ` S)"
  then obtain T where as: "open T" "x \ T" "T \ f ` S" ..
  then have "x \ f ` S" by auto
  then obtain y where y: "y \ S" "x = f y" by auto
  have "open (f -` T)"
    using assms ‹open T› by (simp add: continuous_at_imp_continuous_on open_vimage)
  moreover have "y \ vimage f T"
    using ‹x = f y› ‹x ∈ T› by simp
  moreover have "vimage f T \ S"
    using ‹T ⊆ image f S› ‹inj f› unfolding inj_on_def subset_eq by auto
  ultimately have "y \ interior S" ..
  with ‹x = f y› show "x \ f ` interior S" ..
qed

subsection🍋‹tag unimportant› ‹Equality of continuous functions on closure and related results›

lemma continuous_closedin_preimage_constant:
  fixes f :: "_ \ 'b::t1_space"
  shows "continuous_on S f \ closedin (top_of_set S) {x \ S. f x = a}"
  using continuous_closedin_preimage[of S f "{a}"] by (simp add: vimage_def Collect_conj_eq)

lemma continuous_closed_preimage_constant:
  fixes f :: "_ \ 'b::t1_space"
  shows "continuous_on S f \ closed S \ closed {x \ S. f x = a}"
  using continuous_closed_preimage[of S f "{a}"] by (simp add: vimage_def Collect_conj_eq)

lemma continuous_constant_on_closure:
  fixes f :: "_ \ 'b::t1_space"
  assumes "continuous_on (closure S) f"
      and "\x. x \ S \ f x = a"
      and "x \ closure S"
  shows "f x = a"
    using continuous_closed_preimage_constant[of "closure S" f a]
      assms closure_minimal[of S "{x \ closure S. f x = a}"] closure_subset
    by auto

lemma image_closure_subset:
  assumes contf: "continuous_on (closure S) f"
    and "closed T"
    and "(f ` S) \ T"
  shows "f ` (closure S) \ T"
proof -
  have "S \ {x \ closure S. f x \ T}"
    using assms(3) closure_subset by auto
  moreover have "closed (closure S \ f -` T)"
    using continuous_closed_preimage[OF contf] ‹closed T› by auto
  ultimately have "closure S = (closure S \ f -` T)"
    using closure_minimal[of S "(closure S \ f -` T)"] by auto
  then show ?thesis by auto
qed

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🍋‹tag unimportant› ‹A function constant on a set›

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

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

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

lemma constant_on_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🍋‹tag unimportant› ‹Continuity relative to a union.›

lemma continuous_on_Un_local:
    "\closedin (top_of_set (S \ T)) S; closedin (top_of_set (S \ T)) T;
      continuous_on S f; continuous_on T f]
     ==> continuous_on (S ∪ T) f"
  unfolding continuous_on closedin_limpt
  by (metis Lim_trivial_limit Lim_within_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;
       ∧x. [x ∈ S ∧ ¬P x ∨ x ∈ T ∧ P x] ==> f x = g x]
      ==> continuous_on (S ∪ T) (λx. if P x then f x else g x)"
  by (rule continuous_on_Un_local) (auto intro: continuous_on_eq)

lemma continuous_on_cases_le:
  fixes h :: "'a :: topological_space \ real"
  assumes "continuous_on {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🍋‹tag unimportant›‹Inverse function property for open/closed maps›

lemma continuous_on_inverse_open_map:
  assumes contf: "continuous_on S f"
    and imf: "f ` S = T"
    and injf: "\x. x \ S \ g (f x) = x"
    and oo: "\U. openin (top_of_set S) U \ openin (top_of_set T) (f ` U)"
  shows "continuous_on T g"
proof -
  from imf injf have gTS: "g ` T = S"
    by force
  from imf injf have fU: "U \ S \ (f ` U) = T \ g -` U" for U
    by force
  show ?thesis
    by (simp add: continuous_on_open [of T g] gTS) (metis openin_imp_subset fU oo)
qed

lemma continuous_on_inverse_closed_map:
  assumes contf: "continuous_on S f"
    and imf: "f ` S = T"
    and injf: "\x. x \ S \ g(f x) = x"
    and oo: "\U. closedin (top_of_set S) U \ closedin (top_of_set T) (f ` U)"
  shows "continuous_on T g"
proof -
  from imf injf have gTS: "g ` T = S"
    by force
  from imf injf have fU: "U \ S \ (f ` U) = T \ g -` U" for U
    by force
  show ?thesis
    by (simp add: continuous_on_closed [of T g] gTS) (metis closedin_imp_subset fU oo)
qed

lemma homeomorphism_injective_open_map:
  assumes contf: "continuous_on S f"
    and imf: "f ` S = T"
    and injf: "inj_on f S"
    and oo: "\U. openin (top_of_set S) U \ openin (top_of_set T) (f ` U)"
  obtains g where "homeomorphism S T f g"
proof
  have "continuous_on T (inv_into S f)"
    by (metis contf continuous_on_inverse_open_map imf injf inv_into_f_f oo)
  with imf injf contf show "homeomorphism S T f (inv_into S f)"
    by (auto simp: homeomorphism_def)
qed

lemma homeomorphism_injective_closed_map:
  assumes contf: "continuous_on S f"
    and imf: "f ` S = T"
    and injf: "inj_on f S"
    and oo: "\U. closedin (top_of_set S) U \ closedin (top_of_set T) (f ` U)"
  obtains g where "homeomorphism S T f g"
proof
  have "continuous_on T (inv_into S f)"
    by (metis contf continuous_on_inverse_closed_map imf injf inv_into_f_f oo)
  with imf injf contf show "homeomorphism S T f (inv_into S f)"
    by (auto simp: homeomorphism_def)
qed

lemma homeomorphism_imp_open_map:
  assumes hom: "homeomorphism S T f g"
    and oo: "openin (top_of_set S) U"
  shows "openin (top_of_set T) (f ` U)"
proof -
  from hom oo have [simp]: "f ` U = T \ g -` U"
    using openin_subset by (fastforce simp: homeomorphism_def rev_image_eqI)
  from hom have "continuous_on T g"
    unfolding homeomorphism_def by blast
  moreover have "g ` T = S"
    by (metis hom homeomorphism_def)
  ultimately show ?thesis
    by (simp add: continuous_on_open oo)
qed

lemma homeomorphism_imp_closed_map:
  assumes hom: "homeomorphism S T f g"
    and oo: "closedin (top_of_set S) U"
  shows "closedin (top_of_set T) (f ` U)"
proof -
  from hom oo have [simp]: "f ` U = T \ g -` U"
    using closedin_subset by (fastforce simp: homeomorphism_def rev_image_eqI)
  from hom have "continuous_on T g"
    unfolding homeomorphism_def by blast
  moreover have "g ` T = S"
    by (metis hom homeomorphism_def)
  ultimately show ?thesis
    by (simp add: continuous_on_closed oo)
qed

subsection🍋‹tag unimportant› ‹Seperability›

lemma subset_second_countable:
  obtains B :: "'a:: second_countable_topology set set"
    where "countable \"
          "{} \ \"
          "\C. C \ \ \ openin(top_of_set S) C"
          "\T. openin(top_of_set S) T \ \\. \ \ \ \ T = \\"
proof -
  obtain B :: "'a set set"
    where "countable \"
      and opeB: "\C. C \ \ \ openin(top_of_set S) C"
      and B:    "\T. openin(top_of_set S) T \ \\. \ \ \ \ T = \\"
  proof -
    obtain C :: "'a set set"
      where "countable \" and ope: "\C. C \ \ \ open C"
        and C: "\S. open S \ \U. U \ \ \ S = \U"
      by (metis univ_second_countable that)
    show ?thesis
    proof
      show "countable ((\C. S \ C) ` \)"
        by (simp add: ‹countable C›)
      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 ‹countable B› by blast
    show "\C. \C \ \ - {{}}\ \ openin (top_of_set S) C"
      by (simp add: ‹∧C. C ∈ B ==> openin (top_of_set S) C›)
    show "\\\\ - {{}}. T = \\" if "openin (top_of_set S) T" for T
      using B [OF that]
      by (metis Int_Diff Int_lower2 Union_insert inf.orderE insert_Diff_single sup_bot_left)
  qed auto
qed

lemma Lindelof_openin:
  fixes F :: "'a::second_countable_topology set set"
  assumes "\S. S \ \ \ openin (top_of_set U) S"
  obtains F' where "\' ⊆ F" "countable F'" "\\' = ∪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 \ \ \ \ tf ` \" "\\ = \(tf ` \)"
    using tf by (force intro: Lindelof [of "tf ` \"])
  then obtain F' where \': "\' \ \" "countable \'" "\\' = \\"
    by (clarsimp simp add: countable_subset_image)
  then show ?thesis ..
qed


subsection🍋‹tag unimportant›‹Closed Maps›

lemma continuous_imp_closed_map:
  fixes f :: "'a::t2_space \ 'b::t2_space"
  assumes "closedin (top_of_set S) U"
          "continuous_on S f" "f ` S = T" "compact S"
    shows "closedin (top_of_set T) (f ` U)"
  by (metis assms closedin_compact_eq compact_continuous_image continuous_on_subset subset_image_iff)

lemma closed_map_restrict:
  assumes cloU: "closedin (top_of_set (S \ f -` T')) U"
    and cc: "\U. closedin (top_of_set S) U \ closedin (top_of_set T) (f ` U)"
    and "T' \ T"
  shows "closedin (top_of_set T') (f ` U)"
proof -
  obtain V where "closed V" "U = S \ f -` T' \ V"
    using cloU by (auto simp: closedin_closed)
  with cc [of "S \ V"] ‹T' \ T\ show ?thesis
    by (fastforce simp add: closedin_closed)
qed

subsection🍋‹tag unimportant›‹Open Maps›

lemma open_map_restrict:
  assumes opeU: "openin (top_of_set (S \ f -` T')) U"
    and oo: "\U. openin (top_of_set S) U \ openin (top_of_set T) (f ` U)"
    and "T' \ T"
  shows "openin (top_of_set T') (f ` U)"
proof -
  obtain V where "open V" "U = S \ f -` T' \ V"
    using opeU by (auto simp: openin_open)
  with oo [of "S \ V"] ‹T' \ T\ show ?thesis
    by (fastforce simp add: openin_open)
qed


subsection🍋‹tag unimportant›‹Quotient maps›

lemma quotient_map_imp_continuous_open:
  assumes T: "f \ S \ T"
      and ope: "\U. U \ T
              ==> (openin (top_of_set S) (S ∩ f -` U) ⟷ openin (top_of_set T) U)"
    shows "continuous_on S f"
proof -
  have [simp]: "S \ f -` f ` S = S" by auto
  show ?thesis
    by (meson T continuous_on_open_gen ope openin_imp_subset)
qed

lemma quotient_map_imp_continuous_closed:
  assumes T: "f \ S \ T"
      and ope: "\U. U \ T
                  ==> (closedin (top_of_set S) (S ∩ f -` U) ⟷
                       closedin (top_of_set T) U)"
    shows "continuous_on S f"
proof -
  have [simp]: "S \ f -` f ` S = S" by auto
  show ?thesis
    by (meson T closedin_imp_subset continuous_on_closed_gen ope)
qed

lemma open_map_imp_quotient_map:
  assumes contf: "continuous_on S f"
      and T: "T \ f ` S"
      and ope: "\T. openin (top_of_set S) T
                   ==> openin (top_of_set (f ` S)) (f ` T)"
    shows "openin (top_of_set S) (S \ f -` T) =
           openin (top_of_set (f ` S)) T"
proof -
  have "T = f ` (S \ f -` T)"
    using T by blast
  then show ?thesis
    using "ope" contf continuous_on_open by metis
qed

lemma closed_map_imp_quotient_map:
  assumes contf: "continuous_on S f"
      and T: "T \ f ` S"
      and ope: "\T. closedin (top_of_set S) T
              ==> closedin (top_of_set (f ` S)) (f ` T)"
    shows "openin (top_of_set S) (S \ f -` T) \ openin (top_of_set (f ` S)) T"
          (is "?lhs = ?rhs")
proof
  assume ?lhs
  then have *: "closedin (top_of_set S) (S - (S \ f -` T))"
    using closedin_diff by fastforce
  have [simp]: "(f ` S - f ` (S - (S \ f -` T))) = T"
    using T by blast
  show ?rhs
    using ope [OF *, unfolded closedin_def] by auto
next
  assume ?rhs
  with contf show ?lhs
    by (auto simp: continuous_on_open)
qed

lemma continuous_right_inverse_imp_quotient_map:
  assumes contf: "continuous_on S f" and imf: "f \ S \ T"
      and contg: "continuous_on T g" and img: "g \ T \ S"
      and fg [simp]: "\y. y \ T \ f(g y) = y"
      and U: "U \ T"
    shows "openin (top_of_set S) (S \ f -` U) \ openin (top_of_set T) U"
          (is "?lhs = ?rhs")
proof -
  have f: "\Z. openin (top_of_set (f ` S)) Z \
                openin (top_of_set S) (S ∩ f -` Z)"
  and  g: "\Z. openin (top_of_set (g ` T)) Z \
                openin (top_of_set T) (T ∩ g -` Z)"
    using contf contg by (auto simp: continuous_on_open)
  show ?thesis
  proof
    have "T \ g -` (g ` T \ (S \ f -` U)) = {x \ T. f (g x) \ U}"
      using imf img by blast
    also have "... = U"
      using U by auto
    finally have eq: "T \ g -` (g ` T \ (S \ f -` U)) = U" .
    assume ?lhs
    then have *: "openin (top_of_set (g ` T)) (g ` T \ (S \ f -` U))"
      by (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🍋‹tag unimportant›‹Pasting lemmas for functions, for of casewise definitions›

subsubsection‹on open sets›

lemma pasting_lemma:
  assumes ope: "\i. i \ I \ openin X (T i)"
      and cont: "\i. i \ I \ continuous_map(subtopology X (T i)) Y (f i)"
      and f: "\i j x. \i \ I; j \ I; x \ topspace X \ T i \ T j\ \ f i x = f j x"
      and g: "\x. x \ topspace X \ \j. j \ I \ x \ T j \ g x = f j x"
    shows "continuous_map X Y g"
  unfolding continuous_map_openin_preimage_eq
proof (intro conjI allI impI)
  show "g \ topspace X \ topspace Y"
    using g cont continuous_map_image_subset_topspace by fastforce
next
  fix U
  assume Y: "openin Y U"
  have T: "T i \ topspace X" if "i \ I" for i
    using ope by (simp add: openin_subset that)
  have *: "topspace X \ g -` U = (\i \ I. T i \ f i -` U)"
    using f g T by fastforce
  have "\i. i \ I \ openin X (T i \ f i -` U)"
    using cont unfolding continuous_map_openin_preimage_eq
    by (metis Y T inf.commute inf_absorb1 ope topspace_subtopology openin_trans_full)
  then show "openin X (topspace X \ g -` U)"
    by (auto simp: *)
qed

lemma pasting_lemma_exists:
  assumes X: "topspace X \ (\i \ I. T i)"
      and ope: "\i. i \ I \ openin X (T i)"
      and cont: "\i. i \ I \ continuous_map (subtopology X (T i)) Y (f i)"
      and f: "\i j x. \i \ I; j \ I; x \ topspace X \ T i \ T j\ \ f i x = f j x"
    obtains g where "continuous_map X Y g" "\x i. \i \ I; x \ topspace X \ T i\ \ g x = f i x"
proof
  let ?h = "\x. f (SOME i. i \ I \ x \ T i) x"
  have "\x. x \ topspace X \
         ∃j. j ∈ I ∧ x ∈ T j ∧ f (SOME i. i ∈ I ∧ x ∈ 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 \ {}}
           ⊆ (λi. T i ∩ f i -` U) ` {i ∈ I. T i ∩ V ≠ {}}" for V
    by auto
  have 1: "(\i\I. T i \ f i -` U) \ topspace X"
    using T by blast
  then have "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‹Likewise on closed sets, with a finiteness assumption›

lemma pasting_lemma_closed:
  assumes fin: "finite I"
    and clo: "\i. i \ I \ closedin X (T i)"
    and cont:  "\i. i \ I \ continuous_map(subtopology X (T i)) Y (f i)"
    and f: "\i j x. \i \ I; j \ I; x \ topspace X \ T i \ T j\ \ f i x = f j x"
    and g: "\x. x \ topspace X \ \j. j \ I \ x \ T j \ g x = f j x"
  shows "continuous_map X Y g"
  using pasting_lemma_locally_finite [OF _ clo cont f g] fin by auto

lemma pasting_lemma_exists_locally_finite:
  assumes fin: "\x. x \ topspace X \ \V. openin X V \ x \ V \ finite {i \ I. T i \ V \ {}}"
    and X: "topspace X \ \(T ` I)"
    and clo: "\i. i \ I \ closedin X (T i)"
    and cont:  "\i. i \ I \ continuous_map(subtopology X (T i)) Y (f i)"
    and f: "\i j x. \i \ I; j \ I; x \ topspace X \ T i \ T j\ \ f i x = f j x"
    and g: "\x. x \ topspace X \ \j. j \ I \ x \ T j \ g x = f j x"
  obtains g where "continuous_map X Y g" "\x i. \i \ I; x \ topspace X \ T i\ \ g x = f i x"
proof
  have "\x. x \ topspace X \
         ∃j. j ∈ I ∧ x ∈ T j ∧ f (SOME i. i ∈ I ∧ x ∈ 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 \
         ∃j. j ∈ I ∧ x ∈ T j ∧ f (SOME i. i ∈ I ∧ x ∈ T i) x = f j x"
    by (metis (mono_tags, lifting) UN_iff X someI_ex subset_iff)
  with pasting_lemma_closed [OF ‹finite I› 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 ‹Retractions›

definition🍋‹tag important› retraction :: "('a::topological_space) set \ 'a set \ ('a \ 'a) \ bool"
where "retraction S T r \
  T ⊆ S ∧ continuous_on S r ∧ r ∈ S → T ∧ (∀x∈T. r x = x)"

definition🍋‹tag important› retract_of (infixl ‹retract'_of\ 50) where
"T retract_of S \ (\r. retraction S T r)"

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

text ‹Preservation of fixpoints under (more general notion of) retraction›

lemma invertible_fixpoint_property:
  fixes S :: "'a::topological_space set"
    and T :: "'b::topological_space set"
  assumes contt: "continuous_on T i"
    and "i \ T \ S"
    and contr: "continuous_on S r"
    and "r \ S \ T"
    and ri: "\y. y \ T \ r (i y) = y"
    and FP: "\f. \continuous_on S f; f \ S \ S\ \ \x\S. f x = x"
    and contg: "continuous_on T g"
    and "g \ T \ T"
  obtains y where "y \ T" and "g y = y"
proof -
  have "\x\S. (i \ g \ r) x = x"
  proof (rule FP)
    show "continuous_on S (i \ g \ r)"
      by (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)) \
         (∀g. continuous_on T g ∧ g ∈ T → T ⟶ (∃y∈T. g y = y))"
         (is "?lhs = ?rhs")
proof -
  obtain r i where r:
      "\x\S. i (r x) = x" "r ` S = T" "continuous_on S r"
      "\y\T. r (i y) = y" "i ` T = S" "continuous_on T i"
    using assms unfolding homeomorphic_def homeomorphism_def  by blast
  show ?thesis
  proof
    assume ?lhs
    with r 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: 🍋 ‹yields properties normalized wrt. simp -- less likely to loop›
  assumes "retraction S T r"
  obtains "T = r ` S" "r \ S \ S" "continuous_on S r" "\x. x \ S \ r (r x) = r x"
proof (rule that)
  from retraction [of S T r] assms
  have "T \ S" "continuous_on S r" "r ` S = T" and "\x \ T. r x = x"
    by simp_all
  then show  "r \ S \ S" "continuous_on S r"
    by auto
  then show "T = r ` S"
    using ‹r ` S = T› by blast
  from ‹∀x ∈ T. r x = x› have "r x = x" if "x \ T" for x
    using that by simp
  with ‹r ` S = T› show "r (r x) = r x" if "x \ S" for x
    using that by auto
qed

lemma retract_ofE: 🍋 ‹yields properties normalized wrt. simp -- less likely to loop›
  assumes "T retract_of S"
  obtains r where "T = r ` S" "r \ S \ S" "continuous_on S r" "\x. x \ S \ r (r x) = r x"
proof -
  from assms obtain r where "retraction S T r"
    by (auto simp add: retract_of_def)
  with that show thesis
    by (auto elim: retractionE)
qed

lemma retract_of_imp_extensible:
  assumes "S retract_of T" and "continuous_on S f" and "f \ S \ U"
  obtains g where "continuous_on T g" "g \ T \ U" "\x. x \ S \ g x = f x"
proof -
  from ‹S retract_of T› obtain r where 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 ‹f ∈ S → U› 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) ‹U ⊆ T› 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‹Retractions on a topological space›

definition retract_of_space :: "'a set \ 'a topology \ bool" (infix ‹retract'_of'_space› 50)
  where "S retract_of_space X
         ≡ S ⊆ topspace X ∧ (∃r. continuous_map X (subtopology X S) r ∧ (∀x ∈ S. r x = x))"

lemma retract_of_space_retraction_maps:
   "S retract_of_space X \ S \ topspace X \ (\r. retraction_maps X (subtopology X S) r id)"
  by (auto simp: retract_of_space_def retraction_maps_def)

lemma retract_of_space_section_map:
   "S retract_of_space X \ S \ topspace X \ section_map (subtopology X S) X id"
  unfolding retract_of_space_def retraction_maps_def section_map_def
  by (auto simp: continuous_map_from_subtopology)

lemma retract_of_space_imp_subset:
   "S retract_of_space X \ S \ topspace X"
  by (simp add: retract_of_space_def)

lemma retract_of_space_topspace:
   "topspace X retract_of_space X"
  using retract_of_space_def by force

lemma retract_of_space_empty [simp]:
   "{} retract_of_space X \ 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 ‹S ⊆ topspace X› ‹a ∈ S› by force
      show "x = a" if "x \ X frontier_of {x. x \ S}" for x
        using assms that clopenin_eq_frontier_of by fastforce
    qed
    then show "continuous_map X (subtopology X S) (\x. if x \ S then x else a)"
      using ‹S ⊆ topspace X› ‹a ∈ S›  by (auto simp: continuous_map_in_subtopology)
  qed auto
qed (use assms in auto)

lemma retract_of_space_disjoint_union:
  assumes "openin X S" "openin X T" and ST: "disjnt S T" "S \ T = topspace X" and "S = {} \ 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
        ==> 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‹Paths and path-connectedness›

definition pathin :: "'a topology \ (real \ 'a) \ bool" where
   "pathin X g \ continuous_map (subtopology euclideanreal {0..1}) X g"

lemma pathin_compose:
     "\pathin X g; continuous_map X Y f\ \ pathin Y (f \ g)"
   by (simp add: continuous_map_compose pathin_def)

lemma pathin_subtopology:
     "pathin (subtopology X S) g \ pathin X g \ (\x \ {0..1}. g x \ S)"
  by (auto simp: pathin_def continuous_map_in_subtopology)

lemma pathin_const [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 ⊆ topspace X ∧
        (∀x ∈ S. ∀y ∈ S. ∃g. pathin X g ∧ g ∈ {0..1} → S ∧ g 0 = x ∧ g 1 = y)"
  unfolding path_connectedin_def path_connected_space_def pathin_def continuous_map_in_subtopology
  by (intro conj_cong refl ball_cong) (simp_all add: inf.absorb_iff2 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 ‹x ∈ S› 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 ‹pathin X g› f pathin_compose by auto
    qed (use g in auto)
  qed
qed

lemma path_connectedin_discrete_topology:
  "path_connectedin (discrete_topology U) S \ S \ U \ (\a. S \ {a})" (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‹Connected components›

definition connected_component_of :: "'a topology \ 'a \ 'a \ bool"
  where "connected_component_of X x y \
        ∃T. connectedin X T ∧ x ∈ T ∧ y ∈ T"

abbreviation connected_component_of_set
  where "connected_component_of_set X x \ Collect (connected_component_of X x)"

definition connected_components_of :: "'a topology \ ('a set) set"
  where "connected_components_of X \ connected_component_of_set X ` topspace X"

lemma connected_component_in_topspace:
   "connected_component_of X x y \ x \ topspace X \ y \ topspace X"
  by (meson connected_component_of_def connectedin_subset_topspace in_mono)

lemma connected_component_of_refl:
   "connected_component_of X x x \ x \ topspace X"
  by (meson connected_component_in_topspace connected_component_of_def connectedin_sing insertI1)

lemma connected_component_of_sym:
   "connected_component_of X x y \ connected_component_of X y x"
  by (meson connected_component_of_def)

lemma connected_component_of_trans:
   "\connected_component_of X x y; connected_component_of X y z\
        ==> connected_component_of X x z"
  unfolding connected_component_of_def
  using connectedin_Un by blast

lemma connected_component_of_mono:
   "\connected_component_of (subtopology X S) x y; S \ T\
        ==> connected_component_of (subtopology X T) x y"
  by (metis connected_component_of_def connectedin_subtopology inf.absorb_iff2 subtopology_subtopology)

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

--> maximum size reached

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