# 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 ≠ {})"
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)")
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
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)"
by (metis connected_component_def connected_component_in connected_connected_component mem_Collect_eq subsetI subset_antisym)

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"

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"

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)"
show "connected (closure (connected_component_set S x))"
show "closure (connected_component_set S x) ⊆ S"
by (simp add: S closure_minimal connected_component_subset)
qed
qed

lemma connected_component_disjoint:
"connected_component_set S a ∩ connected_component_set S b = {} ⟷
a ∉ connected_component_set S b"
by (smt (verit) connected_component_eq connected_component_eq_empty connected_component_refl_eq
disjoint_iff_not_equal mem_Collect_eq)

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)"

lemma connected_component_idemp:
"connected_component_set (connected_component_set S x) x = connected_component_set S x"
by (metis Int_absorb connected_component_disjoint connected_component_eq_empty connected_component_eq_self connected_connected_component)

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 (meson connected_component_maximal connected_component_subset connected_connected_component 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"
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" (is "?lhs = ?rhs")
proof -
have "y ∈ ?lhs ⟷ y ∈ ?rhs" for y
by (smt (verit, best) assms connected_component_homeomorphism_iff homeomorphism_def image_iff mem_Collect_eq)
thus ?thesis
by blast
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"

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"
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_uniqueI components_iff connected_component_eq_empty connected_component_maximal connected_component_subset connected_connected_component subset_emptyI)
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 = {}"

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 (smt (verit, best) Int_Un_eq(4) Un_upper1 bot_eq_sup_iff connected_Un in_components_maximal inf.orderE 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

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)
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
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