Quelle  Connected.thy   Sprache: Isabelle

(*  Author:     L C Paulson, University of Cambridge
    Material split off from Topology_Euclidean_Space
*)

chapter ‹Connected Components›

theory Connected
  imports
    Abstract_Topology_2
begin

subsection🍋‹tag unimportant› ‹Connectedness›

lemma connected_local:
 "connected S \
  ¬ (∃e1 e2.
      openin (top_of_set S) e1 ∧
      openin (top_of_set S) e2 ∧
      S ⊆ e1 ∪ e2 ∧
      e1 ∩ e2 = {} ∧
      e1 ≠ {} ∧
      e2 ≠ {})"
  using connected_openin by blast

lemma exists_diff:
  fixes P :: "'a set \ bool"
  shows "(\S. P (- S)) \ (\S. P S)"
  by (metis boolean_algebra_class.boolean_algebra.double_compl)

lemma connected_clopen: "connected S \
  (∀T. openin (top_of_set S) T ∧
     closedin (top_of_set S) T ⟶ T = {} ∨ T = S)" (is "?lhs ⟷ ?rhs")
proof -
  have "\ connected S \
    (∃e1 e2. open e1 ∧ open (- e2) ∧ S ⊆ e1 ∪ (- e2) ∧ e1 ∩ (- e2) ∩ S = {} ∧ e1 ∩ S ≠ {} ∧ (- e2) ∩ S ≠ {})"
    unfolding connected_def openin_open closedin_closed
    by (metis double_complement)
  then have th0: "connected S \
    ¬ (∃e2 e1. closed e2 ∧ open e1 ∧ S ⊆ e1 ∪ (- e2) ∧ e1 ∩ (- e2) ∩ S = {} ∧ e1 ∩ S ≠ {} ∧ (- e2) ∩ S ≠ {})"
    (is " _ \ \ (\e2 e1. ?P e2 e1)")
    unfolding closed_def by metis
  have th1: "?rhs \ \ (\t' t. closed t'\t = S\t' \ t\{} \ t\S \ (\t'. open t' \ t = S \ t'))"
    (is "_ \ \ (\t' t. ?Q t' t)")
    unfolding connected_def openin_open closedin_closed by auto
  have "(\e1. ?P e2 e1) \ (\t. ?Q e2 t)" for e2
  proof -
    have "?P e2 e1 \ (\t. closed e2 \ t = S\e2 \ open e1 \ t = S\e1 \ t\{} \ t \ S)" for e1
      by auto
    then show ?thesis
      by metis
  qed
  then show ?thesis
    by (simp add: th0 th1)
qed

subsection ‹Connected components, considered as a connectedness relation or a set›

definition🍋‹tag important› "connected_component S x y \ \T. connected T \ T \ S \ x \ T \ y \ T"

abbreviation "connected_component_set S x \ Collect (connected_component S x)"

lemma connected_componentI:
  "connected T \ T \ S \ x \ T \ y \ T \ connected_component S x y"
  by (auto simp: connected_component_def)

lemma connected_component_in: "connected_component S x y \ x \ S \ y \ S"
  by (auto simp: connected_component_def)

lemma connected_component_refl: "x \ S \ connected_component S x x"
  using connected_component_def connected_sing by blast
 
lemma connected_component_refl_eq [simp]: "connected_component S x x \ x \ S"
  using connected_component_in connected_component_refl by blast

lemma connected_component_sym: "connected_component S x y \ connected_component S y x"
  by (auto simp: connected_component_def)

lemma connected_component_trans:
  "connected_component S x y \ connected_component S y z \ connected_component S x z"
  unfolding connected_component_def
  by (metis Int_iff Un_iff Un_subset_iff equals0D connected_Un)

lemma connected_component_of_subset:
  "connected_component S x y \ S \ T \ connected_component T x y"
  by (auto simp: connected_component_def)

lemma connected_component_Union: "connected_component_set S x = \{T. connected T \ x \ T \ T \ S}"
  by (auto simp: connected_component_def)

lemma connected_connected_component [iff]: "connected (connected_component_set S x)"
  by (auto simp: connected_component_Union intro: connected_Union)

lemma connected_iff_eq_connected_component_set:
  "connected S \ (\x \ S. connected_component_set S x = S)"
proof 
  show "\x\S. connected_component_set S x = S \ connected S"
    by (metis connectedI_const connected_connected_component)
qed (auto simp: connected_component_def)

lemma connected_component_subset: "connected_component_set S x \ S"
  using connected_component_in by blast

lemma connected_component_eq_self: "connected S \ x \ S \ connected_component_set S x = S"
  by (simp add: connected_iff_eq_connected_component_set)

lemma connected_iff_connected_component:
  "connected S \ (\x \ S. \y \ S. connected_component S x y)"
  using connected_component_in by (auto simp: connected_iff_eq_connected_component_set)

lemma connected_component_maximal:
  "x \ T \ connected T \ T \ S \ T \ (connected_component_set S x)"
  using connected_component_eq_self connected_component_of_subset by blast

lemma connected_component_mono:
  "S \ T \ connected_component_set S x \ connected_component_set T x"
  by (simp add: Collect_mono connected_component_of_subset)

lemma connected_component_eq_empty [simp]: "connected_component_set S x = {} \ x \ S"
  using connected_component_refl by (fastforce simp: connected_component_in)

lemma connected_component_set_empty [simp]: "connected_component_set {} x = {}"
  using connected_component_eq_empty by blast

lemma connected_component_eq:
  "y \ connected_component_set S x \ (connected_component_set S y = connected_component_set S x)"
  by (metis (no_types, lifting)
      Collect_cong connected_component_sym connected_component_trans mem_Collect_eq)

lemma closed_connected_component:
  assumes S: "closed S"
  shows "closed (connected_component_set S x)"
proof (cases "x \ S")
  case False
  then show ?thesis
    by (metis connected_component_eq_empty closed_empty)
next
  case True
  show ?thesis
    unfolding closure_eq [symmetric]
  proof
    show "closure (connected_component_set S x) \ connected_component_set S x"
    proof (rule connected_component_maximal)
      show "x \ closure (connected_component_set S x)"
        by (simp add: closure_def True)
      show "connected (closure (connected_component_set S x))"
        by (simp add: connected_imp_connected_closure)
      show "closure (connected_component_set S x) \ S"
        by (simp add: S closure_minimal connected_component_subset)
    qed  
  qed (simp add: closure_subset)
qed

lemma connected_component_disjoint:
  "connected_component_set S a \ connected_component_set S b = {} \
    a ∉ connected_component_set S b"
  using connected_component_eq connected_component_sym by fastforce

lemma connected_component_nonoverlap:
  "connected_component_set S a \ connected_component_set S b = {} \
    a ∉ S ∨ b ∉ S ∨ connected_component_set S a ≠ connected_component_set S b"
  by (metis connected_component_disjoint connected_component_eq connected_component_eq_empty inf.idem)

lemma connected_component_overlap:
  "connected_component_set S a \ connected_component_set S b \ {} \
    a ∈ S ∧ b ∈ S ∧ connected_component_set S a = connected_component_set S b"
  by (auto simp: connected_component_nonoverlap)

lemma connected_component_sym_eq: "connected_component S x y \ connected_component S y x"
  using connected_component_sym by blast

lemma connected_component_eq_eq:
  "connected_component_set S x = connected_component_set S y \
    x ∉ S ∧ y ∉ S ∨ x ∈ S ∧ y ∈ S ∧ connected_component S x y"
  by (metis connected_component_eq connected_component_eq_empty connected_component_refl mem_Collect_eq)


lemma connected_iff_connected_component_eq:
  "connected S \ (\x \ S. \y \ S. connected_component_set S x = connected_component_set S y)"
  by (simp add: connected_component_eq_eq connected_iff_connected_component)

lemma connected_component_idemp:
  "connected_component_set (connected_component_set S x) x = connected_component_set S x"
proof
  show "connected_component_set S x \ connected_component_set (connected_component_set S x) x"
    by (metis connected_component_eq_empty connected_component_maximal order.refl
        connected_component_refl connected_connected_component mem_Collect_eq)
qed (simp add: connected_component_subset)

lemma connected_component_unique:
  "\x \ c; c \ S; connected c;
    ∧c'. \x \ c'; c' \ S; connected c'] ==> c' \ c\
        ==> connected_component_set S x = c"
  by (simp add: connected_component_maximal connected_component_subset subsetD
      subset_antisym)

lemma joinable_connected_component_eq:
  "\connected T; T \ S;
    connected_component_set S x ∩ T ≠ {};
    connected_component_set S y ∩ T ≠ {}]
    ==> connected_component_set S x = connected_component_set S y"
  by (metis (full_types) subsetD connected_component_eq connected_component_maximal disjoint_iff_not_equal)

lemma Union_connected_component: "\(connected_component_set S ` S) = S"
proof
  show "\(connected_component_set S ` S) \ S"
    by (simp add: SUP_least connected_component_subset)
qed (use connected_component_refl_eq in force)

lemma complement_connected_component_unions:
    "S - connected_component_set S x =
     ∪(connected_component_set S ` S - {connected_component_set S x})"
    (is "?lhs = ?rhs")
proof
  show "?lhs \ ?rhs"
    by (metis Diff_subset Diff_subset_conv Sup_insert Union_connected_component insert_Diff_single)
  show "?rhs \ ?lhs"
    by clarsimp (metis connected_component_eq_eq connected_component_in)
qed

lemma connected_component_intermediate_subset:
        "\connected_component_set U a \ T; T \ U\
        ==> connected_component_set T a = connected_component_set U a"
  by (metis connected_component_idemp connected_component_mono subset_antisym)

lemma connected_component_homeomorphismI:
  assumes "homeomorphism A B f g" "connected_component A x y"
  shows   "connected_component B (f x) (f y)"
proof -
  from assms obtain T where T: "connected T" "T \ A" "x \ T" "y \ T"
    unfolding connected_component_def by blast
  have "connected (f ` T)" "f ` T \ B" "f x \ f ` T" "f y \ f ` T"
    using assms T continuous_on_subset[of A f T]
    by (auto intro!: connected_continuous_image simp: homeomorphism_def)
  thus ?thesis
    unfolding connected_component_def by blast
qed

lemma connected_component_homeomorphism_iff:
  assumes "homeomorphism A B f g"
  shows   "connected_component A x y \ x \ A \ y \ A \ connected_component B (f x) (f y)"
  by (metis assms connected_component_homeomorphismI connected_component_in homeomorphism_apply1 homeomorphism_sym)

lemma connected_component_set_homeomorphism:
  assumes "homeomorphism A B f g" "x \ A"
  shows   "connected_component_set B (f x) = f ` connected_component_set A x"
proof -
  have "\y. connected_component B (f x) y
          ==> ∃u. u ∈ A ∧ connected_component B (f x) (f u) ∧ y = f u"
    using assms by (metis connected_component_in homeomorphism_def image_iff)
  with assms show ?thesis
    by (auto simp: image_iff connected_component_homeomorphism_iff)
qed

subsection ‹The set of connected components of a set›

definition🍋‹tag important› components:: "'a::topological_space set \ 'a set set"
  where "components S \ connected_component_set S ` S"

lemma components_iff: "S \ components U \ (\x. x \ U \ S = connected_component_set U x)"
  by (auto simp: components_def)

lemma componentsI: "x \ U \ connected_component_set U x \ components U"
  by (auto simp: components_def)

lemma componentsE:
  assumes "S \ components U"
  obtains x where "x \ U" "S = connected_component_set U x"
  using assms by (auto simp: components_def)

lemma Union_components [simp]: "\(components U) = U"
  by (simp add: Union_connected_component components_def)

lemma pairwise_disjoint_components: "pairwise (\X Y. X \ Y = {}) (components U)"
  unfolding pairwise_def
  by (metis (full_types) components_iff connected_component_nonoverlap)

lemma in_components_nonempty: "C \ components S \ C \ {}"
    by (metis components_iff connected_component_eq_empty)

lemma in_components_subset: "C \ components S \ C \ S"
  using Union_components by blast

lemma in_components_connected: "C \ components S \ connected C"
  by (metis components_iff connected_connected_component)

lemma in_components_maximal:
  "C \ components S \
    C ≠ {} ∧ C ⊆ S ∧ connected C ∧ (∀D. D ≠ {} ∧ C ⊆ D ∧ D ⊆ S ∧ connected D ⟶ D = C)"
(is "?lhs \ ?rhs")
proof
  assume L: ?lhs
  then have "C \ S" "connected C"
    by (simp_all add: in_components_subset in_components_connected)
  then show ?rhs
    by (metis (full_types) L components_iff connected_component_maximal connected_component_refl empty_iff mem_Collect_eq subsetD subset_antisym)
next
  show "?rhs \ ?lhs"
    by (metis bot.extremum componentsI connected_component_maximal connected_component_subset
        connected_connected_component order_antisym_conv subset_iff)
qed


lemma joinable_components_eq:
  "connected T \ T \ S \ c1 \ components S \ c2 \ components S \ c1 \ T \ {} \ c2 \ T \ {} \ c1 = c2"
  by (metis (full_types) components_iff joinable_connected_component_eq)

lemma closed_components: "\closed S; C \ components S\ \ closed C"
  by (metis closed_connected_component components_iff)

lemma components_nonoverlap:
    "\C \ components S; C' \ components S\ \ (C \ C' = {}) \ (C \ C')"
  by (metis (full_types) components_iff connected_component_nonoverlap)

lemma components_eq: "\C \ components S; C' \ components S\ \ (C = C' \ C \ C' \ {})"
  by (metis components_nonoverlap)

lemma components_eq_empty [simp]: "components S = {} \ S = {}"
  by (simp add: components_def)

lemma components_empty [simp]: "components {} = {}"
  by simp

lemma connected_eq_connected_components_eq: "connected S \ (\C \ components S. \C' \ components S. C = C')"
  by (metis (no_types, opaque_lifting) components_iff connected_component_eq_eq connected_iff_connected_component)

lemma components_eq_sing_iff: "components S = {S} \ connected S \ S \ {}" (is "?lhs \ ?rhs")
proof
  show "?rhs \ ?lhs"
    by (metis components_iff connected_component_eq_self equals0I insert_iff mk_disjoint_insert)
qed (use in_components_connected in fastforce)

lemma components_eq_sing_exists: "(\a. components S = {a}) \ connected S \ S \ {}"
  by (metis Union_components ccpo_Sup_singleton components_eq_sing_iff)

lemma connected_eq_components_subset_sing: "connected S \ components S \ {S}"
  by (metis components_eq_empty components_eq_sing_iff connected_empty subset_singleton_iff)

lemma connected_eq_components_subset_sing_exists: "connected S \ (\a. components S \ {a})"
  by (metis components_eq_sing_exists connected_eq_components_subset_sing subset_singleton_iff)

lemma in_components_self: "S \ components S \ connected S \ S \ {}"
  by (metis components_empty components_eq_sing_iff empty_iff in_components_connected insertI1)

lemma components_maximal: "\C \ components S; connected T; T \ S; C \ T \ {}\ \ T \ C"
  by (metis (lifting) ext Int_Un_eq(4) Int_absorb Un_upper1 bot_eq_sup_iff connected_Un
      in_components_maximal sup.mono sup.orderI)

lemma exists_component_superset: "\T \ S; S \ {}; connected T\ \ \C. C \ components S \ T \ C"
  by (meson componentsI connected_component_maximal equals0I subset_eq)

lemma components_intermediate_subset: "\S \ components U; S \ T; T \ U\ \ S \ components T"
  by (smt (verit, best) dual_order.trans in_components_maximal)

lemma in_components_unions_complement: "C \ components S \ S - C = \(components S - {C})"
  by (metis complement_connected_component_unions components_def components_iff)

lemma connected_intermediate_closure:
  assumes cs: "connected S" and st: "S \ T" and ts: "T \ closure S"
  shows "connected T"
  using assms unfolding connected_def
  by (smt (verit) Int_assoc inf.absorb_iff2 inf_bot_left open_Int_closure_eq_empty)

lemma closedin_connected_component: "closedin (top_of_set S) (connected_component_set S x)"
proof (cases "connected_component_set S x = {}")
  case True
  then show ?thesis
    by (metis closedin_empty)
next
  case False
  then obtain y where y: "connected_component S x y" and "x \ S"
    using connected_component_eq_empty by blast
  have *: "connected_component_set S x \ S \ closure (connected_component_set S x)"
    by (auto simp: closure_def connected_component_in)
  have **: "x \ closure (connected_component_set S x)"
    by (simp add: ‹x ∈ S› closure_def)
  have "S \ closure (connected_component_set S x) \ connected_component_set S x" if "connected_component S x y"
  proof (rule connected_component_maximal)
    show "connected (S \ closure (connected_component_set S x))"
      using "*" connected_intermediate_closure by blast
  qed (use ‹x ∈ S› ** in auto)
  with y * show ?thesis
    by (auto simp: closedin_closed)
qed

lemma closedin_component:
   "C \ components S \ closedin (top_of_set S) C"
  using closedin_connected_component componentsE by blast


subsection🍋‹tag unimportant› ‹Proving a function is constant on a connected set
  by proving that a level set is open›

lemma continuous_levelset_openin_cases:
  fixes f :: "_ \ 'b::t1_space"
  shows "connected S \ continuous_on S f \
        openin (top_of_set S) {x ∈ S. f x = a}
        ==> (∀x ∈ S. f x ≠ a) ∨ (∀x ∈ S. f x = a)"
  unfolding connected_clopen
  using continuous_closedin_preimage_constant by auto

lemma continuous_levelset_openin:
  fixes f :: "_ \ 'b::t1_space"
  shows "connected S \ continuous_on S f \
        openin (top_of_set S) {x ∈ S. f x = a} ==>
        (∃x ∈ S. f x = a)  ==> (∀x ∈ S. f x = a)"
  using continuous_levelset_openin_cases[of S f ]
  by meson

lemma continuous_levelset_open:
  fixes f :: "_ \ 'b::t1_space"
  assumes S: "connected S" "continuous_on S f"
    and a: "open {x \ S. f x = a}" "\x \ S. f x = a"
  shows "\x \ S. f x = a"
  using a continuous_levelset_openin[OF S, of a, unfolded openin_open]
  by fast


subsection🍋‹tag unimportant› ‹Preservation of Connectedness›

lemma homeomorphic_connectedness:
  assumes "S homeomorphic T"
  shows "connected S \ connected T"
using assms unfolding homeomorphic_def homeomorphism_def by (metis connected_continuous_image)

lemma connected_monotone_quotient_preimage:
  assumes "connected T"
      and contf: "continuous_on S f" and fim: "f ` S = T"
      and opT: "\U. U \ T
                 ==> openin (top_of_set S) (S ∩ f -` U) ⟷
                     openin (top_of_set T) U"
      and connT: "\y. y \ T \ connected (S \ f -` {y})"
    shows "connected S"
proof (rule connectedI)
  fix U V
  assume "open U" and "open V" and "U \ S \ {}" and "V \ S \ {}"
    and "U \ V \ S = {}" and "S \ U \ V"
  moreover
  have disjoint: "f ` (S \ U) \ f ` (S \ V) = {}"
  proof -
    have False if "y \ f ` (S \ U) \ f ` (S \ V)" for y
    proof -
      have "y \ T"
        using fim that by blast
      show ?thesis
        using connectedD [OF connT [OF ‹y ∈ T›] ‹open U› ‹open V›]
              ‹S ⊆ U ∪ V› ‹U ∩ V ∩ S = {}› that by fastforce
    qed
    then show ?thesis by blast
  qed
  ultimately have UU: "(S \ f -` f ` (S \ U)) = S \ U" and VV: "(S \ f -` f ` (S \ V)) = S \ V"
    by auto
  have opeU: "openin (top_of_set T) (f ` (S \ U))"
    by (metis UU ‹open U› fim image_Int_subset le_inf_iff opT openin_open_Int)
  have opeV: "openin (top_of_set T) (f ` (S \ V))"
    by (metis opT fim VV ‹open V› openin_open_Int image_Int_subset inf.bounded_iff)
  have "T \ f ` (S \ U) \ f ` (S \ V)"
    using ‹S ⊆ U ∪ V› fim by auto
  then show False
    using ‹connected T› disjoint opeU opeV ‹U ∩ S ≠ {}› ‹V ∩ S ≠ {}›
    by (auto simp: connected_openin)
qed

lemma connected_open_monotone_preimage:
  assumes contf: "continuous_on S f" and fim: "f ` S = T"
    and ST: "\C. openin (top_of_set S) C \ openin (top_of_set T) (f ` C)"
    and connT: "\y. y \ T \ connected (S \ f -` {y})"
    and "connected C" "C \ T"
  shows "connected (S \ f -` C)"
proof -
  have contf': "continuous_on (S \ f -` C) f"
    by (meson contf continuous_on_subset inf_le1)
  have eqC: "f ` (S \ f -` C) = C"
    using ‹C ⊆ T› fim by blast
  show ?thesis
  proof (rule connected_monotone_quotient_preimage [OF ‹connected C› contf' eqC])
    show "connected (S \ f -` C \ f -` {y})" if "y \ C" for y
      by (metis Int_assoc Int_empty_right Int_insert_right_if1 assms(6) connT in_mono that vimage_Int)
    have "\U. openin (top_of_set (S \ f -` C)) U
               ==> openin (top_of_set C) (f ` U)"
      using open_map_restrict [OF _ ST ‹C ⊆ T›] by metis
    then show "\D. D \ C
          ==> openin (top_of_set (S ∩ f -` C)) (S ∩ f -` C ∩ f -` D) =
              openin (top_of_set C) D"
      using open_map_imp_quotient_map [of "(S \ f -` C)" f] contf' by (simp add: eqC)
  qed
qed


lemma connected_closed_monotone_preimage:
  assumes contf: "continuous_on S f" and fim: "f ` S = T"
    and ST: "\C. closedin (top_of_set S) C \ closedin (top_of_set T) (f ` C)"
    and connT: "\y. y \ T \ connected (S \ f -` {y})"
    and "connected C" "C \ T"
  shows "connected (S \ f -` C)"
proof -
  have contf': "continuous_on (S \ f -` C) f"
    by (meson contf continuous_on_subset inf_le1)
  have eqC: "f ` (S \ f -` C) = C"
    using ‹C ⊆ T› fim by blast
  show ?thesis
  proof (rule connected_monotone_quotient_preimage [OF ‹connected C› contf' eqC])
    show "connected (S \ f -` C \ f -` {y})" if "y \ C" for y
      by (metis Int_assoc Int_empty_right Int_insert_right_if1 ‹C ⊆ T› connT subsetD that vimage_Int)
    have "\U. closedin (top_of_set (S \ f -` C)) U
               ==> closedin (top_of_set C) (f ` U)"
      using closed_map_restrict [OF _ ST ‹C ⊆ T›] by metis
    then show "\D. D \ C
          ==> openin (top_of_set (S ∩ f -` C)) (S ∩ f -` C ∩ f -` D) =
              openin (top_of_set C) D"
      using closed_map_imp_quotient_map [of "(S \ f -` C)" f] contf' by (simp add: eqC)
  qed
qed


subsection‹Lemmas about components›

text  ‹See Newman IV, 3.3 and 3.4.›

lemma connected_Un_clopen_in_complement:
  fixes S U :: "'a::metric_space set"
  assumes "connected S" "connected U" "S \ U" 
      and opeT: "openin (top_of_set (U - S)) T" 
      and cloT: "closedin (top_of_set (U - S)) T"
    shows "connected (S \ T)"
proof -
  have *: "\\x y. P x y \ P y x; \x y. P x y \ S \ x \ S \ y;
            ∧x y. [P x y; S ⊆ x] ==> False] ==> ¬(∃x y. (P x y))" for P
    by metis
  show ?thesis
    unfolding connected_closedin_eq
  proof (rule *)
    fix H1 H2
    assume H: "closedin (top_of_set (S \ T)) H1 \
               closedin (top_of_set (S ∪ T)) H2 ∧
               H1 ∪ H2 = S ∪ T ∧ H1 ∩ H2 = {} ∧ H1 ≠ {} ∧ H2 ≠ {}"
    then have clo: "closedin (top_of_set S) (S \ H1)"
                   "closedin (top_of_set S) (S \ H2)"
      by (metis Un_upper1 closedin_closed_subset inf_commute)+
    moreover have "S \ ((S \ T) \ H1) \ S \ ((S \ T) \ H2) = S"
      using H by blast
    moreover have "H1 \ (S \ ((S \ T) \ H2)) = {}"
      using H by blast
    ultimately have "S \ H1 = {} \ S \ H2 = {}"
      by (smt (verit) Int_assoc ‹connected S› connected_closedin_eq inf_commute inf_sup_absorb)
    then show "S \ H1 \ S \ H2"
      using H ‹connected S› unfolding connected_closedin by blast
  next
    fix H1 H2
    assume H: "closedin (top_of_set (S \ T)) H1 \
               closedin (top_of_set (S ∪ T)) H2 ∧
               H1 ∪ H2 = S ∪ T ∧ H1 ∩ H2 = {} ∧ H1 ≠ {} ∧ H2 ≠ {}"
       and "S \ H1"
    then have H2T: "H2 \ T"
      by auto
    have "T \ U"
      using Diff_iff opeT openin_imp_subset by auto
    with ‹S ⊆ U› have Ueq: "U = (U - S) \ (S \ T)" 
      by auto
    have "openin (top_of_set ((U - S) \ (S \ T))) H2"
    proof (rule openin_subtopology_Un)
      show "openin (top_of_set (S \ T)) H2"
        by (metis Diff_cancel H Un_Diff Un_Diff_Int closedin_subset openin_closedin_eq topspace_euclidean_subtopology)
      then show "openin (top_of_set (U - S)) H2"
        by (meson H2T Un_upper2 opeT openin_subset_trans openin_trans)
    qed
    moreover have "closedin (top_of_set ((U - S) \ (S \ T))) H2"
    proof (rule closedin_subtopology_Un)
      show "closedin (top_of_set (U - S)) H2"
        using H H2T cloT closedin_subset_trans 
        by (blast intro: closedin_subtopology_Un closedin_trans)
    qed (simp add: H)
    ultimately have H2: "H2 = {} \ H2 = U"
      using Ueq ‹connected U› unfolding connected_clopen by metis   
    then have "H2 \ S"
      by (metis Diff_partition H Un_Diff_cancel Un_subset_iff ‹H2 ⊆ T› assms(3) inf.orderE opeT openin_imp_subset)
    moreover have "T \ H2 - S"
      by (metis (no_types) H2 H opeT openin_closedin_eq topspace_euclidean_subtopology)
    ultimately show False
      using H ‹S ⊆ H1› by blast
  qed blast
qed


proposition component_diff_connected:
  fixes S :: "'a::metric_space set"
  assumes "connected S" "connected U" "S \ U" and C: "C \ components (U - S)"
  shows "connected(U - C)"
  using ‹connected S› unfolding connected_closedin_eq not_ex de_Morgan_conj
proof clarify
  fix H3 H4 
  assume clo3: "closedin (top_of_set (U - C)) H3" 
    and clo4: "closedin (top_of_set (U - C)) H4" 
    and H34: "H3 \ H4 = U - C" "H3 \ H4 = {}" and "H3 \ {}" and "H4 \ {}"
    and * [rule_format]: "\H1 H2. \ closedin (top_of_set S) H1 \
                      ¬ closedin (top_of_set S) H2 ∨
                      H1 ∪ H2 ≠ S ∨ H1 ∩ H2 ≠ {} ∨ ¬ H1 ≠ {} ∨ ¬ H2 ≠ {}"
  then have "H3 \ U-C" and ope3: "openin (top_of_set (U - C)) (U - C - H3)"
    and "H4 \ U-C" and ope4: "openin (top_of_set (U - C)) (U - C - H4)"
    by (auto simp: closedin_def)
  have "C \ {}" "C \ U-S" "connected C"
    using C in_components_nonempty in_components_subset in_components_maximal by blast+
  have cCH3: "connected (C \ H3)"
  proof (rule connected_Un_clopen_in_complement [OF ‹connected C› ‹connected U› _ _ clo3])
    show "openin (top_of_set (U - C)) H3"
      by (metis Diff_cancel Un_Diff Un_Diff_Int ‹H3 ∩ H4 = {}› ‹H3 ∪ H4 = U - C› ope4)
  qed (use clo3 ‹C ⊆ U - S› in auto)
  have cCH4: "connected (C \ H4)"
  proof (rule connected_Un_clopen_in_complement [OF ‹connected C› ‹connected U› _ _ clo4])
    show "openin (top_of_set (U - C)) H4"
      by (metis Diff_cancel Diff_triv Int_Un_eq(2) Un_Diff H34 inf_commute ope3)
  qed (use clo4 ‹C ⊆ U - S› in auto)
  have "closedin (top_of_set S) (S \ H3)" "closedin (top_of_set S) (S \ H4)"
    using clo3 clo4 ‹S ⊆ U› ‹C ⊆ U - S› by (auto simp: closedin_closed)
  moreover have "S \ H3 \ {}"      
    using components_maximal [OF C cCH3] ‹C ≠ {}› ‹C ⊆ U - S› ‹H3 ≠ {}› ‹H3 ⊆ U - C› by auto
  moreover have "S \ H4 \ {}"
    using components_maximal [OF C cCH4] ‹C ≠ {}› ‹C ⊆ U - S› ‹H4 ≠ {}› ‹H4 ⊆ U - C› by auto
  ultimately show False
    using * [of "S \ H3" "S \ H4"] ‹H3 ∩ H4 = {}› ‹C ⊆ U - S› ‹H3 ∪ H4 = U - C› ‹S ⊆ U› 
    by auto
qed


subsection🍋‹tag unimportant›‹Constancy of a function from a connected set into a finite, disconnected or discrete set›

text‹Still missing: versions for a set that is smaller than R, or countable.›

lemma continuous_disconnected_range_constant:
  assumes S: "connected S"
      and conf: "continuous_on S f"
      and fim: "f \ S \ T"
      and cct: "\y. y \ T \ connected_component_set T y = {y}"
    shows "f constant_on S"
proof (cases "S = {}")
  case True then show ?thesis
    by (simp add: constant_on_def)
next
  case False
  then have "f ` S \ {f x}" if "x \ S" for x
    by (metis PiE S cct connected_component_maximal connected_continuous_image [OF conf] fim image_eqI 
        image_subset_iff that)
  with False show ?thesis
    unfolding constant_on_def by blast
qed


text‹This proof requires the existence of two separate values of the range type.›
lemma finite_range_constant_imp_connected:
  assumes "\f::'a::topological_space \ 'b::real_normed_algebra_1.
              [continuous_on S f; finite(f ` S)] ==> f constant_on S"
  shows "connected S"
proof -
  { fix T U
    assume clt: "closedin (top_of_set S) T"
       and clu: "closedin (top_of_set S) U"
       and tue: "T \ U = {}" and tus: "T \ U = S"
    have "continuous_on (T \ U) (\x. if x \ T then 0 else 1)"
      using clt clu tue by (intro continuous_on_cases_local) (auto simp: tus)
    then have conif: "continuous_on S (\x. if x \ T then 0 else 1)"
      using tus by blast
    have fi: "finite ((\x. if x \ T then 0 else 1) ` S)"
      by (rule finite_subset [of _ "{0,1}"]) auto
    have "T = {} \ U = {}"
      using assms [OF conif fi] tus [symmetric]
      by (auto simp: Ball_def constant_on_def) (metis IntI empty_iff one_neq_zero tue)
  }
  then show ?thesis
    by (simp add: connected_closedin_eq)
qed

end