Theory Connected

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

section ‹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 ≠ {})"
  unfolding connected_def openin_open
  by safe blast+

lemma exists_diff:
  fixes P :: "'a set ⇒ bool"
  shows "(∃S. P (- S)) ⟷ (∃S. P S)"
    (is "?lhs ⟷ ?rhs")
proof -
  have ?rhs if ?lhs
    using that by blast
  moreover have "P (- (- S))" if "P S" for S
  proof -
    have "S = - (- S)" by simp
    with that show ?thesis by metis
  qed
  ultimately show ?thesis by metis
qed

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)")
    by (simp add: closed_def) 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 have "∀e2. (∃e1. ?P e2 e1) ⟷ (∃t. ?Q e2 t)"
    by blast
  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"
  by (auto simp: connected_component_def) (use connected_sing in blast)

lemma connected_component_refl_eq [simp]: "connected_component S x x ⟷ x ∈ S"
  by (auto simp: connected_component_refl) (auto simp: connected_component_def)

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 (cases "S = {}")
  case True
  then show ?thesis by simp
next
  case False
  then obtain x where "x ∈ S" by auto
  show ?thesis
  proof
    assume "connected S"
    then show "∀x ∈ S. connected_component_set S x = S"
      by (force simp: connected_component_def)
  next
    assume "∀x ∈ S. connected_component_set S x = S"
    then show "connected S"
      by (metis ‹x ∈ S› connected_connected_component)
  qed
qed

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"
      apply (rule connected_component_maximal)
        apply (simp add: closure_def True)
       apply (simp add: connected_imp_connected_closure)
      apply (simp add: S closure_minimal connected_component_subset)
      done
  next
    show "connected_component_set S x ⊆ closure (connected_component_set S x)"
      by (simp add: closure_subset)
  qed
qed

lemma connected_component_disjoint:
  "connected_component_set S a ∩ connected_component_set S b = {} ⟷
    a ∉ connected_component_set S b"
  apply (auto simp: connected_component_eq)
  using connected_component_eq connected_component_sym
  apply blast
  done

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"
  apply (auto simp: connected_component_in)
  using connected_component_refl_eq
    apply blast
   apply (metis connected_component_eq mem_Collect_eq)
  apply (metis connected_component_eq mem_Collect_eq)
  done

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"
  apply (cases "y ∈ S", simp)
   apply (metis connected_component_eq connected_component_eq_empty connected_component_refl_eq mem_Collect_eq)
  apply (cases "x ∈ S", simp)
   apply (metis connected_component_eq_empty)
  using connected_component_eq_empty
  apply blast
  done

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"
  apply (rule subset_antisym)
   apply (simp add: connected_component_subset)
  apply (metis connected_component_eq_empty connected_component_maximal
      connected_component_refl_eq connected_connected_component mem_Collect_eq set_eq_subset)
  done

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"
  apply (rule subset_antisym)
   apply (meson connected_component_maximal connected_component_subset connected_connected_component contra_subsetD)
  by (simp add: connected_component_maximal)

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"
apply (simp add: ex_in_conv [symmetric])
apply (rule connected_component_eq)
by (metis (no_types, hide_lams) connected_component_eq_eq connected_component_in connected_component_maximal subsetD mem_Collect_eq)


lemma Union_connected_component: "⋃(connected_component_set S ` S) = S"
  apply (rule subset_antisym)
  apply (simp add: SUP_least connected_component_subset)
  using connected_component_refl_eq
  by force


lemma complement_connected_component_unions:
    "S - connected_component_set S x =
     ⋃(connected_component_set S ` S - {connected_component_set S x})"
  apply (subst Union_connected_component [symmetric], auto)
  apply (metis connected_component_eq_eq connected_component_in)
  by (metis connected_component_eq mem_Collect_eq)

lemma connected_component_intermediate_subset:
        "⟦connected_component_set U a ⊆ T; T ⊆ U⟧
        ⟹ connected_component_set T a = connected_component_set U a"
  apply (case_tac "a ∈ U")
  apply (simp add: connected_component_maximal connected_component_mono subset_antisym)
  using connected_component_eq_empty by blast


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"
  apply (rule subset_antisym)
  using Union_connected_component components_def apply fastforce
  apply (metis Union_connected_component components_def set_eq_subset)
  done

lemma pairwise_disjoint_components: "pairwise (λX Y. X ∩ Y = {}) (components u)"
  apply (simp add: pairwise_def)
  apply (auto simp: components_iff)
  apply (metis connected_component_eq_eq connected_component_in)+
  done

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)"
  apply (rule iffI)
   apply (simp add: in_components_nonempty in_components_connected)
   apply (metis (full_types) components_iff connected_component_eq_self connected_component_intermediate_subset connected_component_refl in_components_subset mem_Collect_eq rev_subsetD)
  apply (metis bot.extremum_uniqueI components_iff connected_component_eq_empty connected_component_maximal connected_component_subset connected_connected_component subset_emptyI)
  done

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')"
  apply (auto simp: in_components_nonempty components_iff)
    using connected_component_refl apply blast
   apply (metis connected_component_eq_eq connected_component_in)
  by (metis connected_component_eq mem_Collect_eq)

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, hide_lams) components_iff connected_component_eq_eq connected_iff_connected_component)

lemma components_eq_sing_iff: "components s = {s} ⟷ connected s ∧ s ≠ {}"
  apply (rule iffI)
  using in_components_connected apply fastforce
  apply safe
  using Union_components apply fastforce
   apply (metis components_iff connected_component_eq_self)
  using in_components_maximal
  apply auto
  done

lemma components_eq_sing_exists: "(∃a. components s = {a}) ⟷ connected s ∧ s ≠ {}"
  apply (rule iffI)
  using connected_eq_connected_components_eq apply fastforce
  apply (metis components_eq_sing_iff)
  done

lemma connected_eq_components_subset_sing: "connected s ⟷ components s ⊆ {s}"
  by (metis Union_components components_empty components_eq_sing_iff connected_empty insert_subset order_refl subset_singletonD)

lemma connected_eq_components_subset_sing_exists: "connected s ⟷ (∃a. components s ⊆ {a})"
  by (metis components_eq_sing_exists connected_eq_components_subset_sing empty_iff subset_iff subset_singletonD)

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"
  apply (simp add: components_def ex_in_conv [symmetric], clarify)
  by (meson connected_component_def connected_component_trans)

lemma exists_component_superset: "⟦t ⊆ s; s ≠ {}; connected t⟧ ⟹ ∃c. c ∈ components s ∧ t ⊆ c"
  apply (cases "t = {}", force)
  apply (metis components_def ex_in_conv connected_component_maximal contra_subsetD image_eqI)
  done

lemma components_intermediate_subset: "⟦s ∈ components u; s ⊆ t; t ⊆ u⟧ ⟹ s ∈ components t"
  apply (auto simp: components_iff)
  apply (metis connected_component_eq_empty connected_component_intermediate_subset)
  done

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"
proof (rule connectedI)
  fix A B
  assume A: "open A" and B: "open B" and Alap: "A ∩ t ≠ {}" and Blap: "B ∩ t ≠ {}"
    and disj: "A ∩ B ∩ t = {}" and cover: "t ⊆ A ∪ B"
  have disjs: "A ∩ B ∩ s = {}"
    using disj st by auto
  have "A ∩ closure s ≠ {}"
    using Alap Int_absorb1 ts by blast
  then have Alaps: "A ∩ s ≠ {}"
    by (simp add: A open_Int_closure_eq_empty)
  have "B ∩ closure s ≠ {}"
    using Blap Int_absorb1 ts by blast
  then have Blaps: "B ∩ s ≠ {}"
    by (simp add: B open_Int_closure_eq_empty)
  then show False
    using cs [unfolded connected_def] A B disjs Alaps Blaps cover st
    by blast
qed

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"
    by blast
  have *: "connected_component_set s x ⊆ s ∩ closure (connected_component_set s x)"
    by (auto simp: closure_def connected_component_in)
  have "connected_component s x y ⟹ s ∩ closure (connected_component_set s x) ⊆ connected_component_set s x"
    apply (rule connected_component_maximal, simp)
    using closure_subset connected_component_in apply fastforce
    using * connected_intermediate_closure apply blast+
    done
  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 "connected s"
    and "continuous_on s f"
    and "open {x ∈ s. f x = a}"
    and "∃x ∈ s.  f x = a"
  shows "∀x ∈ s. f x = a"
  using continuous_levelset_openin[OF assms(1,2), of a, unfolded openin_open]
  using assms (3,4)
  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
    proof -
      have "S ∩ f -` C ∩ f -` {y} = S ∩ f -` {y}"
        using that by blast
      moreover have "connected (S ∩ f -` {y})"
        using ‹C ⊆ T› connT that by blast
      ultimately show ?thesis
        by metis
    qed
    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
    proof -
      have "S ∩ f -` C ∩ f -` {y} = S ∩ f -` {y}"
        using that by blast
      moreover have "connected (S ∩ f -` {y})"
        using ‹C ⊆ T› connT that by blast
      ultimately show ?thesis
        by metis
    qed
    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)+
    have Seq: "S ∩ (H1 ∪ H2) = S"
      by (simp add: H)
    have "S ∩ ((S ∪ T) ∩ H1) ∪ S ∩ ((S ∪ T) ∩ H2) = S"
      using Seq by auto
    moreover have "H1 ∩ (S ∩ ((S ∪ T) ∩ H2)) = {}"
      using H by blast
    ultimately have "S ∩ H1 = {} ∨ S ∩ H2 = {}"
      by (metis (no_types) H Int_assoc ‹S ∩ (H1 ∪ H2) = S› ‹connected S›
          clo Seq connected_closedin inf_bot_right inf_le1)
    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"
        using ‹H2 ⊆ T› apply (auto simp: openin_closedin_eq)
        by (metis Diff_Diff_Int Diff_disjoint Diff_partition Diff_subset H Int_absorb1 Un_Diff)
      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 "H3 ∪ H4 = U - C" and "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"
      apply (simp add: openin_closedin_eq ‹H3 ⊆ U - C›)
      apply (simp add: closedin_subtopology)
      by (metis Diff_cancel Diff_triv Un_Diff clo4 ‹H3 ∩ H4 = {}› ‹H3 ∪ H4 = U - C› closedin_closed inf_commute sup_bot.left_neutral)
  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"
      apply (simp add: openin_closedin_eq ‹H4 ⊆ U - C›)
      apply (simp add: closedin_subtopology)
      by (metis Diff_cancel Int_commute Un_Diff Un_Diff_Int ‹H3 ∩ H4 = {}› ‹H3 ∪ H4 = U - C› clo3 closedin_closed)
  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
  { fix x assume "x ∈ S"
    then have "f ` S ⊆ {f x}"
    by (metis connected_continuous_image conf connected_component_maximal fim image_subset_iff rev_image_eqI S cct)
  }
  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 conif: "continuous_on S (λx. if x ∈ t then 0 else 1)"
      apply (subst tus [symmetric])
      apply (rule continuous_on_cases_local)
      using clt clu tue
      apply (auto simp: tus)
      done
    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