Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Connected.thy Sprache: Isabelle

Original von: Isabelle^©

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

section \<open>Connected Components\<close>

theory Connected
  imports
    Abstract_Topology_2
begin

subsection\<^marker>\<open>tag unimportant\<close> \<open>Connectedness\<close>

lemma connected_local:
"connected S \
  \<not> (\<exists>e1 e2.
      openin (top_of_set S) e1 \<and>
      openin (top_of_set S) e2 \<and>
      S \<subseteq> e1 \<union> e2 \<and>
      e1 \<inter> e2 = {} \<and>
      e1 \<noteq> {} \<and>
      e2 \<noteq> {})"
  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 \
  (\<forall>T. openin (top_of_set S) T \<and>
     closedin (top_of_set S) T \<longrightarrow> T = {} \<or> T = S)" (is "?lhs \<longleftrightarrow> ?rhs")
proof -
  have "\ connected S \
    (\<exists>e1 e2. open e1 \<and> open (- e2) \<and> S \<subseteq> e1 \<union> (- e2) \<and> e1 \<inter> (- e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (- e2) \<inter> S \<noteq> {})"
    unfolding connected_def openin_open closedin_closed
    by (metis double_complement)
  then have th0: "connected S \
    \<not> (\<exists>e2 e1. closed e2 \<and> open e1 \<and> S \<subseteq> e1 \<union> (- e2) \<and> e1 \<inter> (- e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (- e2) \<inter> S \<noteq> {})"
    (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 \<open>Connected components, considered as a connectedness relation or a set\<close>

definition\<^marker>\<open>tag important\<close> "connected_component S x y \<equiv> \<exists>T. connected T \<and> T \<subseteq> S \<and> x \<in> T \<and> y \<in> 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 \<open>x \<in> S\<close> 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 \<notin> 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 \<notin> S \<or> b \<notin> S \<or> connected_component_set S a \<noteq> 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 \<in> S \<and> b \<in> S \<and> 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 \<notin> S \<and> y \<notin> S \<or> x \<in> S \<and> y \<in> S \<and> 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;
    \<And>c'. \<lbrakk>x \<in> c'; c' \<subseteq> S; connected c'\<rbrakk> \<Longrightarrow> c' \<subseteq> c\<rbrakk>
        \<Longrightarrow> 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 \<inter> T \<noteq> {};
    connected_component_set S y \<inter> T \<noteq> {}\<rbrakk>
    \<Longrightarrow> 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 =
     \<Union>(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\
        \<Longrightarrow> 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 \<open>The set of connected components of a set\<close>

definition\<^marker>\<open>tag important\<close> components:: "'a::topological_space set \<Rightarrow> '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 \<noteq> {} \<and> c \<subseteq> s \<and> connected c \<and> (\<forall>d. d \<noteq> {} \<and> c \<subseteq> d \<and> d \<subseteq> s \<and> connected d \<longrightarrow> 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\<^marker>\<open>tag unimportant\<close> \<open>Proving a function is constant on a connected set
  by proving that a level set is open\<close>

lemma continuous_levelset_openin_cases:
  fixes f :: "_ \ 'b::t1_space"
  shows "connected s \ continuous_on s f \
        openin (top_of_set s) {x \<in> s. f x = a}
        \<Longrightarrow> (\<forall>x \<in> s. f x \<noteq> a) \<or> (\<forall>x \<in> 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 \<in> s. f x = a} \<Longrightarrow>
        (\<exists>x \<in> s. f x = a)  \<Longrightarrow> (\<forall>x \<in> 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\<^marker>\<open>tag unimportant\<close> \<open>Preservation of Connectedness\<close>

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
                 \<Longrightarrow> openin (top_of_set S) (S \<inter> f -` U) \<longleftrightarrow>
                     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 \<open>y \<in> T\<close>] \<open>open U\<close> \<open>open V\<close>]
              \<open>S \<subseteq> U \<union> V\<close> \<open>U \<inter> V \<inter> S = {}\<close> 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>open U\<close> 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>open V\<close> openin_open_Int image_Int_subset inf.bounded_iff)
  have "T \ f ` (S \ U) \ f ` (S \ V)"
    using \<open>S \<subseteq> U \<union> V\<close> fim by auto
  then show False
    using \<open>connected T\<close> disjoint opeU opeV \<open>U \<inter> S \<noteq> {}\<close> \<open>V \<inter> S \<noteq> {}\<close>
    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 \<open>C \<subseteq> T\<close> fim by blast
  show ?thesis
  proof (rule connected_monotone_quotient_preimage [OF \<open>connected C\<close> 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 \<open>C \<subseteq> T\<close> connT that by blast
      ultimately show ?thesis
        by metis
    qed
    have "\U. openin (top_of_set (S \ f -` C)) U
               \<Longrightarrow> openin (top_of_set C) (f ` U)"
      using open_map_restrict [OF _ ST \<open>C \<subseteq> T\<close>] by metis
    then show "\D. D \ C
          \<Longrightarrow> openin (top_of_set (S \<inter> f -` C)) (S \<inter> f -` C \<inter> 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 \<open>C \<subseteq> T\<close> fim by blast
  show ?thesis
  proof (rule connected_monotone_quotient_preimage [OF \<open>connected C\<close> 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 \<open>C \<subseteq> T\<close> connT that by blast
      ultimately show ?thesis
        by metis
    qed
    have "\U. closedin (top_of_set (S \ f -` C)) U
               \<Longrightarrow> closedin (top_of_set C) (f ` U)"
      using closed_map_restrict [OF _ ST \<open>C \<subseteq> T\<close>] by metis
    then show "\D. D \ C
          \<Longrightarrow> openin (top_of_set (S \<inter> f -` C)) (S \<inter> f -` C \<inter> 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\<open>Lemmas about components\<close>

text  \<open>See Newman IV, 3.3 and 3.4.\<close>

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;
            \<And>x y. \<lbrakk>P x y; S \<subseteq> x\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> \<not>(\<exists>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 \<union> T)) H2 \<and>
               H1 \<union> H2 = S \<union> T \<and> H1 \<inter> H2 = {} \<and> H1 \<noteq> {} \<and> H2 \<noteq> {}"
    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 \<open>S \<inter> (H1 \<union> H2) = S\<close> \<open>connected S\<close>
          clo Seq connected_closedin inf_bot_right inf_le1)
    then show "S \ H1 \ S \ H2"
      using H \<open>connected S\<close> unfolding connected_closedin by blast
  next
    fix H1 H2
    assume H: "closedin (top_of_set (S \ T)) H1 \
               closedin (top_of_set (S \<union> T)) H2 \<and>
               H1 \<union> H2 = S \<union> T \<and> H1 \<inter> H2 = {} \<and> H1 \<noteq> {} \<and> H2 \<noteq> {}"
       and "S \ H1"
    then have H2T: "H2 \ T"
      by auto
    have "T \ U"
      using Diff_iff opeT openin_imp_subset by auto
    with \<open>S \<subseteq> U\<close> have Ueq: "U = (U - S) \<union> (S \<union> 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 \<open>H2 \<subseteq> T\<close> 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 \<open>connected U\<close> unfolding connected_clopen by metis
    then have "H2 \ S"
      by (metis Diff_partition H Un_Diff_cancel Un_subset_iff \<open>H2 \<subseteq> T\<close> 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 \<open>S \<subseteq> H1\<close> 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 \<open>connected S\<close> 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 \
                      \<not> closedin (top_of_set S) H2 \<or>
                      H1 \<union> H2 \<noteq> S \<or> H1 \<inter> H2 \<noteq> {} \<or> \<not> H1 \<noteq> {} \<or> \<not> H2 \<noteq> {}"
  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 \<open>connected C\<close> \<open>connected U\<close> _ _ clo3])
    show "openin (top_of_set (U - C)) H3"
      apply (simp add: openin_closedin_eq \<open>H3 \<subseteq> U - C\<close>)
      apply (simp add: closedin_subtopology)
      by (metis Diff_cancel Diff_triv Un_Diff clo4 \<open>H3 \<inter> H4 = {}\<close> \<open>H3 \<union> H4 = U - C\<close> closedin_closed inf_commute sup_bot.left_neutral)
  qed (use clo3 \<open>C \<subseteq> U - S\<close> in auto)
  have cCH4: "connected (C \ H4)"
  proof (rule connected_Un_clopen_in_complement [OF \<open>connected C\<close> \<open>connected U\<close> _ _ clo4])
    show "openin (top_of_set (U - C)) H4"
      apply (simp add: openin_closedin_eq \<open>H4 \<subseteq> U - C\<close>)
      apply (simp add: closedin_subtopology)
      by (metis Diff_cancel Int_commute Un_Diff Un_Diff_Int \<open>H3 \<inter> H4 = {}\<close> \<open>H3 \<union> H4 = U - C\<close> clo3 closedin_closed)
  qed (use clo4 \<open>C \<subseteq> U - S\<close> in auto)
  have "closedin (top_of_set S) (S \ H3)" "closedin (top_of_set S) (S \ H4)"
    using clo3 clo4 \<open>S \<subseteq> U\<close> \<open>C \<subseteq> U - S\<close> by (auto simp: closedin_closed)
  moreover have "S \ H3 \ {}"
    using components_maximal [OF C cCH3] \<open>C \<noteq> {}\<close> \<open>C \<subseteq> U - S\<close> \<open>H3 \<noteq> {}\<close> \<open>H3 \<subseteq> U - C\<close> by auto
  moreover have "S \ H4 \ {}"
    using components_maximal [OF C cCH4] \<open>C \<noteq> {}\<close> \<open>C \<subseteq> U - S\<close> \<open>H4 \<noteq> {}\<close> \<open>H4 \<subseteq> U - C\<close> 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\<^marker>\<open>tag unimportant\<close>\<open>Constancy of a function from a connected set into a finite, disconnected or discrete set\<close>

text\<open>Still missing: versions for a set that is smaller than R, or countable.\<close>

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\<open>This proof requires the existence of two separate values of the range type.\<close>
lemma finite_range_constant_imp_connected:
  assumes "\f::'a::topological_space \ 'b::real_normed_algebra_1.
              \<lbrakk>continuous_on S f; finite(f ` S)\<rbrakk> \<Longrightarrow> 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

¤ Dauer der Verarbeitung: 0.25 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.