Quelle Jordan_Curve.thy Sprache: Isabelle

(*  Title:      HOL/Analysis/Jordan_Curve.thy
    Authors:    LC Paulson, based on material from HOL Light
*)

section \<open>The Jordan Curve Theorem and Applications\<close>

theory Jordan_Curve
  imports Arcwise_Connected Further_Topology
begin

subsection\<open>Janiszewski's theorem\<close>

lemma Janiszewski_weak:
  fixes a b::complex
  assumes "compact S" "compact T" and conST: "connected(S \ T)"
      and ccS: "connected_component (- S) a b" and ccT: "connected_component (- T) a b"
    shows "connected_component (- (S \ T)) a b"
proof -
  have [simp]: "a \ S" "a \ T" "b \ S" "b \ T"
    by (meson ComplD ccS ccT connected_component_in)+
  have clo: "closedin (top_of_set (S \ T)) S" "closedin (top_of_set (S \ T)) T"
    by (simp_all add: assms closed_subset compact_imp_closed)
  obtain g where contg: "continuous_on S g"
             and g: "\x. x \ S \ exp (\* of_real (g x)) = (x - a) /\<^sub>R cmod (x - a) / ((x - b) /\<^sub>R cmod (x - b))"
    using ccS \<open>compact S\<close>
    apply (simp add: Borsuk_maps_homotopic_in_connected_component_eq [symmetric])
    apply (subst (asm) homotopic_circlemaps_divide)
    apply (auto simp: inessential_eq_continuous_logarithm_circle)
    done
  obtain h where conth: "continuous_on T h"
             and h: "\x. x \ T \ exp (\* of_real (h x)) = (x - a) /\<^sub>R cmod (x - a) / ((x - b) /\<^sub>R cmod (x - b))"
    using ccT \<open>compact T\<close>
    apply (simp add: Borsuk_maps_homotopic_in_connected_component_eq [symmetric])
    apply (subst (asm) homotopic_circlemaps_divide)
    apply (auto simp: inessential_eq_continuous_logarithm_circle)
    done
  have "continuous_on (S \ T) (\x. (x - a) /\<^sub>R cmod (x - a))" "continuous_on (S \ T) (\x. (x - b) /\<^sub>R cmod (x - b))"
    by (intro continuous_intros; force)+
  moreover have "(\x. (x - a) /\<^sub>R cmod (x - a)) ` (S \ T) \ sphere 0 1" "(\x. (x - b) /\<^sub>R cmod (x - b)) ` (S \ T) \ sphere 0 1"
    by (auto simp: divide_simps)
  moreover have "\g. continuous_on (S \ T) g \
                     (\<forall>x\<in>S \<union> T. (x - a) /\<^sub>R cmod (x - a) / ((x - b) /\<^sub>R cmod (x - b)) = exp (\<i>*complex_of_real (g x)))"
  proof (cases "S \ T = {}")
    case True
    then have "continuous_on (S \ T) (\x. if x \ S then g x else h x)"
      using continuous_on_cases_local [OF clo contg conth]
      by (meson disjoint_iff)
    then show ?thesis
      by (rule_tac x="(\x. if x \ S then g x else h x)" in exI) (auto simp: g h)
  next
    case False
    have diffpi: "\n. g x = h x + 2* of_int n*pi" if "x \ S \ T" for x
    proof -
      have "exp (\* of_real (g x)) = exp (\* of_real (h x))"
        using that by (simp add: g h)
      then obtain n where "complex_of_real (g x) = complex_of_real (h x) + 2* of_int n*complex_of_real pi"
        apply (simp add: exp_eq)
        by (metis complex_i_not_zero distrib_left mult.commute mult_cancel_left)
      then show ?thesis
        using of_real_eq_iff by (fastforce intro!: exI [where x=n])
    qed
    have contgh: "continuous_on (S \ T) (\x. g x - h x)"
      by (intro continuous_intros continuous_on_subset [OF contg] continuous_on_subset [OF conth]) auto
    moreover have disc:
          "\e>0. \y. y \ S \ T \ g y - h y \ g x - h x \ e \ norm ((g y - h y) - (g x - h x))"
          if "x \ S \ T" for x
    proof -
      obtain nx where nx: "g x = h x + 2* of_int nx*pi"
        using \<open>x \<in> S \<inter> T\<close> diffpi by blast
      have "2*pi \ norm (g y - h y - (g x - h x))" if y: "y \ S \ T" and neq: "g y - h y \ g x - h x" for y
      proof -
        obtain ny where ny: "g y = h y + 2* of_int ny*pi"
          using \<open>y \<in> S \<inter> T\<close> diffpi by blast
        { assume "nx \ ny"
          then have "1 \ \real_of_int ny - real_of_int nx\"
            by linarith
          then have "(2*pi)*1 \ (2*pi)*\real_of_int ny - real_of_int nx\"
            by simp
          also have "... = \2*real_of_int ny*pi - 2*real_of_int nx*pi\"
            by (simp add: algebra_simps abs_if)
          finally have "2*pi \ \2*real_of_int ny*pi - 2*real_of_int nx*pi\" by simp
        }
        with neq show ?thesis
          by (simp add: nx ny)
      qed
      then show ?thesis
        by (rule_tac x="2*pi" in exI) auto
    qed
    ultimately have "(\x. g x - h x) constant_on S \ T"
      using continuous_discrete_range_constant [OF conST contgh] by blast
    then obtain z where z: "\x. x \ S \ T \ g x - h x = z"
      by (auto simp: constant_on_def)
    obtain w where "exp(\ * of_real(h w)) = exp (\ * of_real(z + h w))"
      using disc z False
      by auto (metis diff_add_cancel g h of_real_add)
    then have [simp]: "exp (\* of_real z) = 1"
      by (metis cis_conv_exp cis_mult exp_not_eq_zero mult_cancel_right1)
    show ?thesis
    proof (intro exI conjI)
      show "continuous_on (S \ T) (\x. if x \ S then g x else z + h x)"
        by (intro continuous_intros continuous_on_cases_local [OF clo contg] conth) (use z in force)
    qed (auto simp: g h algebra_simps exp_add)
  qed
  ultimately have "homotopic_with_canon (\x. True) (S \ T) (sphere 0 1)
                          (\<lambda>x. (x - a) /\<^sub>R cmod (x - a))  (\<lambda>x. (x - b) /\<^sub>R cmod (x - b))"
    by (subst homotopic_circlemaps_divide) (auto simp: inessential_eq_continuous_logarithm_circle)
  moreover have "compact (S \ T)"
    using assms by blast
  ultimately show ?thesis
    using assms Borsuk_maps_homotopic_in_connected_component_eq by fastforce
qed

theorem Janiszewski:
  fixes a b :: complex
  assumes "compact S" "closed T" and conST: "connected (S \ T)"
      and ccS: "connected_component (- S) a b" and ccT: "connected_component (- T) a b"
    shows "connected_component (- (S \ T)) a b"
proof -
  have "path_component(- T) a b"
    by (simp add: \<open>closed T\<close> ccT open_Compl open_path_connected_component)
  then obtain g where g: "path g" "path_image g \ - T" "pathstart g = a" "pathfinish g = b"
    by (auto simp: path_component_def)
  then obtain C where C: "compact C" "connected C" "a \ C" "b \ C" "C \ T = {}"
    by fastforce
  obtain r where "0 < r" and r: "C \ S \ ball 0 r"
    by (metis \<open>compact C\<close> \<open>compact S\<close> bounded_Un compact_imp_bounded bounded_subset_ballD)
  have "connected_component (- (S \ (T \ cball 0 r \ sphere 0 r))) a b"
  proof (rule Janiszewski_weak [OF \<open>compact S\<close>])
    show comT': "compact ((T \ cball 0 r) \ sphere 0 r)"
      by (simp add: \<open>closed T\<close> closed_Int_compact compact_Un)
    have "S \ (T \ cball 0 r \ sphere 0 r) = S \ T"
      using r by auto
    with conST show "connected (S \ (T \ cball 0 r \ sphere 0 r))"
      by simp
    show "connected_component (- (T \ cball 0 r \ sphere 0 r)) a b"
      using conST C r
      apply (simp add: connected_component_def)
      apply (rule_tac x=C in exI)
      by auto
  qed (simp add: ccS)
  then obtain U where U: "connected U" "U \ - S" "U \ - T \ - cball 0 r" "U \ - sphere 0 r" "a \ U" "b \ U"
    by (auto simp: connected_component_def)
  show ?thesis
    unfolding connected_component_def
  proof (intro exI conjI)
    show "U \ - (S \ T)"
      using U r \<open>0 < r\<close> \<open>a \<in> C\<close> connected_Int_frontier [of U "cball 0 r"]
      apply simp
      by (metis ball_subset_cball compl_inf disjoint_eq_subset_Compl disjoint_iff_not_equal inf.orderE inf_sup_aci(3) subsetCE)
  qed (auto simp: U)
qed

lemma Janiszewski_connected:
  fixes S :: "complex set"
  assumes ST: "compact S" "closed T" "connected(S \ T)"
    and notST: "connected (- S)" "connected (- T)"
  shows "connected(- (S \ T))"
  using Janiszewski [OF ST] by (metis IntD1 IntD2 notST compl_sup connected_iff_connected_component)

subsection\<open>The Jordan Curve theorem\<close>

lemma exists_double_arc:
  fixes g :: "real \ 'a::real_normed_vector"
  assumes "simple_path g" "pathfinish g = pathstart g" "a \ path_image g" "b \ path_image g" "a \ b"
  obtains u d where "arc u" "arc d" "pathstart u = a" "pathfinish u = b"
                    "pathstart d = b" "pathfinish d = a"
                    "(path_image u) \ (path_image d) = {a,b}"
                    "(path_image u) \ (path_image d) = path_image g"
proof -
  obtain u where u: "0 \ u" "u \ 1" "g u = a"
    using assms by (auto simp: path_image_def)
  define h where "h \ shiftpath u g"
  have "simple_path h"
    using \<open>simple_path g\<close> simple_path_shiftpath \<open>0 \<le> u\<close> \<open>u \<le> 1\<close> assms(2) h_def by blast
  have "pathstart h = g u"
    by (simp add: \<open>u \<le> 1\<close> h_def pathstart_shiftpath)
  have "pathfinish h = g u"
    by (simp add: \<open>0 \<le> u\<close> assms h_def pathfinish_shiftpath)
  have pihg: "path_image h = path_image g"
    by (simp add: \<open>0 \<le> u\<close> \<open>u \<le> 1\<close> assms h_def path_image_shiftpath)
  then obtain v where v: "0 \ v" "v \ 1" "h v = b"
    using assms by (metis (mono_tags, lifting) atLeastAtMost_iff imageE path_image_def)
  show ?thesis
  proof
    show "arc (subpath 0 v h)"
      by (metis (no_types) \<open>pathstart h = g u\<close> \<open>simple_path h\<close> arc_simple_path_subpath \<open>a \<noteq> b\<close> atLeastAtMost_iff zero_le_one order_refl pathstart_def u(3) v)
    show "arc (subpath v 1 h)"
      by (metis (no_types) \<open>pathfinish h = g u\<close> \<open>simple_path h\<close> arc_simple_path_subpath \<open>a \<noteq> b\<close> atLeastAtMost_iff zero_le_one order_refl pathfinish_def u(3) v)
    show "pathstart (subpath 0 v h) = a"
      by (metis \<open>pathstart h = g u\<close> pathstart_def pathstart_subpath u(3))
    show "pathfinish (subpath 0 v h) = b"  "pathstart (subpath v 1 h) = b"
      by (simp_all add: v(3))
    show "pathfinish (subpath v 1 h) = a"
      by (metis \<open>pathfinish h = g u\<close> pathfinish_def pathfinish_subpath u(3))
    show "path_image (subpath 0 v h) \ path_image (subpath v 1 h) = {a, b}"
    proof
      have "loop_free h"
        using \<open>simple_path h\<close> simple_path_def by blast
      then show "path_image (subpath 0 v h) \ path_image (subpath v 1 h) \ {a, b}"
        using v \<open>pathfinish (subpath v 1 h) = a\<close>
        apply (clarsimp simp add: loop_free_def path_image_subpath Ball_def)
        by (smt (verit))
      show "{a, b} \ path_image (subpath 0 v h) \ path_image (subpath v 1 h)"
        using v \<open>pathstart (subpath 0 v h) = a\<close> \<open>pathfinish (subpath v 1 h) = a\<close>
        by (auto simp: path_image_subpath image_iff Bex_def)
    qed
    show "path_image (subpath 0 v h) \ path_image (subpath v 1 h) = path_image g"
      using v path_image_subpath pihg path_image_def
      by (metis (full_types) image_Un ivl_disj_un_two_touch(4))
  qed
qed

theorem\<^marker>\<open>tag unimportant\<close> Jordan_curve:
  fixes c :: "real \ complex"
  assumes "simple_path c" and loop: "pathfinish c = pathstart c"
  obtains inner outer where
                "inner \ {}" "open inner" "connected inner"
                "outer \ {}" "open outer" "connected outer"
                "bounded inner" "\ bounded outer" "inner \ outer = {}"
                "inner \ outer = - path_image c"
                "frontier inner = path_image c"
                "frontier outer = path_image c"
proof -
  have "path c"
    by (simp add: assms simple_path_imp_path)
  have hom: "(path_image c) homeomorphic (sphere(0::complex) 1)"
    by (simp add: assms homeomorphic_simple_path_image_circle)
  with Jordan_Brouwer_separation have "\ connected (- (path_image c))"
    by fastforce
  then obtain inner where inner: "inner \ components (- path_image c)" and "bounded inner"
    using cobounded_has_bounded_component [of "- (path_image c)"]
    using \<open>\<not> connected (- path_image c)\<close> \<open>simple_path c\<close> bounded_simple_path_image by force
  obtain outer where outer: "outer \ components (- path_image c)" and "\ bounded outer"
    using cobounded_unbounded_components [of "- (path_image c)"]
    using \<open>path c\<close> bounded_path_image by auto
  show ?thesis
  proof
    show "inner \ {}"
      using inner in_components_nonempty by auto
    show "open inner"
      by (meson \<open>simple_path c\<close> compact_imp_closed compact_simple_path_image inner open_Compl open_components)
    show "connected inner"
      using in_components_connected inner by blast
    show "outer \ {}"
      using outer in_components_nonempty by auto
    show "open outer"
      by (meson \<open>simple_path c\<close> compact_imp_closed compact_simple_path_image outer open_Compl open_components)
    show "connected outer"
      using in_components_connected outer by blast
    show inner_outer: "inner \ outer = {}"
      by (meson \<open>\<not> bounded outer\<close> \<open>bounded inner\<close> \<open>connected outer\<close> bounded_subset components_maximal in_components_subset inner outer)
    show fro_inner: "frontier inner = path_image c"
      by (simp add: Jordan_Brouwer_frontier [OF hom inner])
    show fro_outer: "frontier outer = path_image c"
      by (simp add: Jordan_Brouwer_frontier [OF hom outer])
    have False if m: "middle \ components (- path_image c)" and "middle \ inner" "middle \ outer" for middle
    proof -
      have "frontier middle = path_image c"
        by (simp add: Jordan_Brouwer_frontier [OF hom] that)
      obtain middle: "open middle" "connected middle" "middle \ {}"
        by (metis fro_inner frontier_closed in_components_maximal m open_Compl open_components)
      obtain a0 b0 where "a0 \ path_image c" "b0 \ path_image c" "a0 \ b0"
        using simple_path_image_uncountable [OF \<open>simple_path c\<close>]
        by (metis Diff_cancel countable_Diff_eq countable_empty insert_iff subsetI subset_singleton_iff)
      obtain a b g where ab: "a \ path_image c" "b \ path_image c" "a \ b"
                     and g: "arc g" "pathstart g = a" "pathfinish g = b"
                     and pag_sub: "path_image g - {a,b} \ middle"
      proof (rule dense_accessible_frontier_point_pairs [OF \<open>open middle\<close> \<open>connected middle\<close>, of "path_image c \<inter> ball a0 (dist a0 b0)" "path_image c \<inter> ball b0 (dist a0 b0)"])
        show "openin (top_of_set (frontier middle)) (path_image c \ ball a0 (dist a0 b0))"
             "openin (top_of_set (frontier middle)) (path_image c \ ball b0 (dist a0 b0))"
          by (simp_all add: \<open>frontier middle = path_image c\<close> openin_open_Int)
        show "path_image c \ ball a0 (dist a0 b0) \ path_image c \ ball b0 (dist a0 b0)"
          using \<open>a0 \<noteq> b0\<close> \<open>b0 \<in> path_image c\<close> by auto
        show "path_image c \ ball a0 (dist a0 b0) \ {}"
          using \<open>a0 \<in> path_image c\<close> \<open>a0 \<noteq> b0\<close> by auto
        show "path_image c \ ball b0 (dist a0 b0) \ {}"
          using \<open>b0 \<in> path_image c\<close> \<open>a0 \<noteq> b0\<close> by auto
      qed (use arc_distinct_ends arc_imp_simple_path simple_path_endless that in fastforce)
      obtain u d where "arc u" "arc d"
                   and "pathstart u = a" "pathfinish u = b" "pathstart d = b" "pathfinish d = a"
                   and ud_ab: "(path_image u) \ (path_image d) = {a,b}"
                   and ud_Un: "(path_image u) \ (path_image d) = path_image c"
        using exists_double_arc [OF assms ab] by blast
      obtain x y where "x \ inner" "y \ outer"
        using \<open>inner \<noteq> {}\<close> \<open>outer \<noteq> {}\<close> by auto
      have "inner \ middle = {}" "middle \ outer = {}"
        using components_nonoverlap inner outer m that by blast+
      have "connected_component (- (path_image u \ path_image g \ (path_image d \ path_image g))) x y"
      proof (rule Janiszewski)
        show "compact (path_image u \ path_image g)"
          by (simp add: \<open>arc g\<close> \<open>arc u\<close> compact_Un compact_arc_image)
        show "closed (path_image d \ path_image g)"
          by (simp add: \<open>arc d\<close> \<open>arc g\<close> closed_Un closed_arc_image)
        show "connected ((path_image u \ path_image g) \ (path_image d \ path_image g))"
          using ud_ab
          by (metis Un_insert_left g connected_arc_image insert_absorb pathfinish_in_path_image pathstart_in_path_image sup_bot_left sup_commute sup_inf_distrib1)
        show "connected_component (- (path_image u \ path_image g)) x y"
          unfolding connected_component_def
        proof (intro exI conjI)
          have "connected ((inner \ (path_image c - path_image u)) \ (outer \ (path_image c - path_image u)))"
          proof (rule connected_Un)
            show "connected (inner \ (path_image c - path_image u))"
              using connected_intermediate_closure [OF \<open>connected inner\<close>]
              by (metis Diff_subset closure_Un_frontier dual_order.refl fro_inner sup.mono sup_ge1)
            show "connected (outer \ (path_image c - path_image u))"
              using connected_intermediate_closure [OF \<open>connected outer\<close>]
              by (simp add: Diff_eq closure_Un_frontier fro_outer sup_inf_distrib1)
            have "(inner \ outer) \ (path_image c - path_image u) \ {}"
              using \<open>arc d\<close> \<open>pathfinish d = a\<close> \<open>pathstart d = b\<close> arc_imp_simple_path nonempty_simple_path_endless ud_Un ud_ab by fastforce
            then show "(inner \ (path_image c - path_image u)) \ (outer \ (path_image c - path_image u)) \ {}"
              by auto
          qed
          then show "connected (inner \ outer \ (path_image c - path_image u))"
            by (metis sup.right_idem sup_assoc sup_commute)
          have "inner \ - path_image u" "outer \ - path_image u"
            using in_components_subset inner outer ud_Un by auto
          moreover have "inner \ - path_image g" "outer \ - path_image g"
            using \<open>inner \<inter> middle = {}\<close> \<open>inner \<subseteq> - path_image u\<close>
            using \<open>middle \<inter> outer = {}\<close> \<open>outer \<subseteq> - path_image u\<close> pag_sub ud_ab by fastforce+
          moreover have "path_image c - path_image u \ - path_image g"
            using in_components_subset m pag_sub ud_ab by fastforce
          ultimately show "inner \ outer \ (path_image c - path_image u) \ - (path_image u \ path_image g)"
            by force
          show "x \ inner \ outer \ (path_image c - path_image u)"
            by (auto simp: \<open>x \<in> inner\<close>)
          show "y \ inner \ outer \ (path_image c - path_image u)"
            by (auto simp: \<open>y \<in> outer\<close>)
        qed
        show "connected_component (- (path_image d \ path_image g)) x y"
          unfolding connected_component_def
        proof (intro exI conjI)
          have "connected ((inner \ (path_image c - path_image d)) \ (outer \ (path_image c - path_image d)))"
          proof (rule connected_Un)
            show "connected (inner \ (path_image c - path_image d))"
              using connected_intermediate_closure [OF \<open>connected inner\<close>] fro_inner
              by (simp add: closure_Un_frontier sup.coboundedI2)
            show "connected (outer \ (path_image c - path_image d))"
              using connected_intermediate_closure [OF \<open>connected outer\<close>]
              by (simp add: closure_Un_frontier fro_outer sup.coboundedI2)
            have "(inner \ outer) \ (path_image c - path_image d) \ {}"
              using \<open>arc u\<close> \<open>pathfinish u = b\<close> \<open>pathstart u = a\<close> arc_imp_simple_path nonempty_simple_path_endless ud_Un ud_ab by fastforce
            then show "(inner \ (path_image c - path_image d)) \ (outer \ (path_image c - path_image d)) \ {}"
              by auto
          qed
          then show "connected (inner \ outer \ (path_image c - path_image d))"
            by (metis sup.right_idem sup_assoc sup_commute)
          have "inner \ - path_image d" "outer \ - path_image d"
            using in_components_subset inner outer ud_Un by auto
          moreover have "inner \ - path_image g" "outer \ - path_image g"
            using \<open>inner \<inter> middle = {}\<close> \<open>inner \<subseteq> - path_image d\<close>
            using \<open>middle \<inter> outer = {}\<close> \<open>outer \<subseteq> - path_image d\<close> pag_sub ud_ab by fastforce+
          moreover have "path_image c - path_image d \ - path_image g"
            using in_components_subset m pag_sub ud_ab by fastforce
          ultimately show "inner \ outer \ (path_image c - path_image d) \ - (path_image d \ path_image g)"
            by force
          show "x \ inner \ outer \ (path_image c - path_image d)"
            by (auto simp: \<open>x \<in> inner\<close>)
          show "y \ inner \ outer \ (path_image c - path_image d)"
            by (auto simp: \<open>y \<in> outer\<close>)
        qed
      qed
      then have "connected_component (- (path_image u \ path_image d \ path_image g)) x y"
        by (simp add: Un_ac)
      moreover have "\(connected_component (- (path_image c)) x y)"
        by (metis (no_types, lifting) \<open>\<not> bounded outer\<close> \<open>bounded inner\<close> \<open>x \<in> inner\<close> \<open>y \<in> outer\<close> componentsE connected_component_eq inner mem_Collect_eq outer)
      ultimately show False
        by (auto simp: ud_Un [symmetric] connected_component_def)
    qed
    then have "components (- path_image c) = {inner,outer}"
      using inner outer by blast
    then have "Union (components (- path_image c)) = inner \ outer"
      by simp
    then show "inner \ outer = - path_image c"
      by auto
  qed (auto simp: \<open>bounded inner\<close> \<open>\<not> bounded outer\<close>)
qed

corollary\<^marker>\<open>tag unimportant\<close> Jordan_disconnected:
  fixes c :: "real \ complex"
  assumes "simple_path c" "pathfinish c = pathstart c"
  shows "\ connected(- path_image c)"
  using Jordan_curve [OF assms]
  by (metis Jordan_Brouwer_separation assms homeomorphic_simple_path_image_circle zero_less_one)

corollary Jordan_inside_outside:
  fixes c :: "real \ complex"
  assumes "simple_path c" "pathfinish c = pathstart c"
    shows "inside(path_image c) \ {} \
          open(inside(path_image c)) \<and>
          connected(inside(path_image c)) \<and>
          outside(path_image c) \<noteq> {} \<and>
          open(outside(path_image c)) \<and>
          connected(outside(path_image c)) \<and>
          bounded(inside(path_image c)) \<and>
          \<not> bounded(outside(path_image c)) \<and>
          inside(path_image c) \<inter> outside(path_image c) = {} \<and>
          inside(path_image c) \<union> outside(path_image c) =
          - path_image c \<and>
          frontier(inside(path_image c)) = path_image c \<and>
          frontier(outside(path_image c)) = path_image c"
proof -
  obtain inner outer
    where *: "inner \ {}" "open inner" "connected inner"
             "outer \ {}" "open outer" "connected outer"
             "bounded inner" "\ bounded outer" "inner \ outer = {}"
             "inner \ outer = - path_image c"
             "frontier inner = path_image c"
             "frontier outer = path_image c"
    using Jordan_curve [OF assms] by blast
  then have inner: "inside(path_image c) = inner"
    by (metis dual_order.antisym inside_subset interior_eq interior_inside_frontier)
  have outer: "outside(path_image c) = outer"
    using \<open>inner \<union> outer = - path_image c\<close> \<open>inside (path_image c) = inner\<close>
          outside_inside \<open>inner \<inter> outer = {}\<close> by auto
  show ?thesis
    using * by (auto simp: inner outer)
qed

subsubsection\<open>Triple-curve or "theta-curve" theorem\<close>

text\<open>Proof that there is no fourth component taken from
     Kuratowski's Topology vol 2, para 61, II.\

theorem split_inside_simple_closed_curve:
  fixes c :: "real \ complex"
  assumes "simple_path c1" and c1: "pathstart c1 = a" "pathfinish c1 = b"
      and "simple_path c2" and c2: "pathstart c2 = a" "pathfinish c2 = b"
      and "simple_path c"  and c: "pathstart c = a" "pathfinish c = b"
      and "a \ b"
      and c1c2: "path_image c1 \ path_image c2 = {a,b}"
      and c1c: "path_image c1 \ path_image c = {a,b}"
      and c2c: "path_image c2 \ path_image c = {a,b}"
      and ne_12: "path_image c \ inside(path_image c1 \ path_image c2) \ {}"
  obtains "inside(path_image c1 \ path_image c) \ inside(path_image c2 \ path_image c) = {}"
          "inside(path_image c1 \ path_image c) \ inside(path_image c2 \ path_image c) \
           (path_image c - {a,b}) = inside(path_image c1 \<union> path_image c2)"
proof -
  let ?\<Theta> = "path_image c"  let ?\<Theta>1 = "path_image c1"  let ?\<Theta>2 = "path_image c2"
  have sp: "simple_path (c1 +++ reversepath c2)" "simple_path (c1 +++ reversepath c)" "simple_path (c2 +++ reversepath c)"
    using assms by (auto simp: simple_path_join_loop_eq arc_simple_path simple_path_reversepath)
  then have op_in12: "open (inside (?\1 \ ?\2))"
     and op_out12: "open (outside (?\1 \ ?\2))"
     and op_in1c: "open (inside (?\1 \ ?\))"
     and op_in2c: "open (inside (?\2 \ ?\))"
     and op_out1c: "open (outside (?\1 \ ?\))"
     and op_out2c: "open (outside (?\2 \ ?\))"
     and co_in1c: "connected (inside (?\1 \ ?\))"
     and co_in2c: "connected (inside (?\2 \ ?\))"
     and co_out12c: "connected (outside (?\1 \ ?\2))"
     and co_out1c: "connected (outside (?\1 \ ?\))"
     and co_out2c: "connected (outside (?\2 \ ?\))"
     and pa_c: "?\ - {pathstart c, pathfinish c} \ - ?\1"
               "?\ - {pathstart c, pathfinish c} \ - ?\2"
     and pa_c1: "?\1 - {pathstart c1, pathfinish c1} \ - ?\2"
                "?\1 - {pathstart c1, pathfinish c1} \ - ?\"
     and pa_c2: "?\2 - {pathstart c2, pathfinish c2} \ - ?\1"
                "?\2 - {pathstart c2, pathfinish c2} \ - ?\"
     and co_c: "connected(?\ - {pathstart c,pathfinish c})"
     and co_c1: "connected(?\1 - {pathstart c1,pathfinish c1})"
     and co_c2: "connected(?\2 - {pathstart c2,pathfinish c2})"
     and fr_in: "frontier(inside(?\1 \ ?\2)) = ?\1 \ ?\2"
              "frontier(inside(?\2 \ ?\)) = ?\2 \ ?\"
              "frontier(inside(?\1 \ ?\)) = ?\1 \ ?\"
     and fr_out: "frontier(outside(?\1 \ ?\2)) = ?\1 \ ?\2"
              "frontier(outside(?\2 \ ?\)) = ?\2 \ ?\"
              "frontier(outside(?\1 \ ?\)) = ?\1 \ ?\"
    using Jordan_inside_outside [of "c1 +++ reversepath c2"]
    using Jordan_inside_outside [of "c1 +++ reversepath c"]
    using Jordan_inside_outside [of "c2 +++ reversepath c"] assms
              apply (simp_all add: path_image_join closed_Un closed_simple_path_image open_inside open_outside)
      apply (blast | metis connected_simple_path_endless)+
    done
  have inout_12: "inside (?\1 \ ?\2) \ (?\ - {pathstart c, pathfinish c}) \ {}"
    by (metis (no_types, lifting) c c1c ne_12 Diff_Int_distrib Diff_empty Int_empty_right Int_left_commute inf_sup_absorb inf_sup_aci(1) inside_no_overlap)
  have pi_disjoint:  "?\ \ outside(?\1 \ ?\2) = {}"
  proof (rule ccontr)
    assume "?\ \ outside (?\1 \ ?\2) \ {}"
    then show False
      using connectedD [OF co_c, of "inside(?\1 \ ?\2)" "outside(?\1 \ ?\2)"]
      using c c1c2 pa_c op_in12 op_out12 inout_12
      apply clarsimp
      by (smt (verit, ccfv_threshold) Diff_Int_distrib Diff_cancel Diff_empty Int_assoc inf_sup_absorb inf_sup_aci(1) outside_no_overlap)
  qed
  have out_sub12: "outside(?\1 \ ?\2) \ outside(?\1 \ ?\)" "outside(?\1 \ ?\2) \ outside(?\2 \ ?\)"
    by (metis Un_commute pi_disjoint outside_Un_outside_Un)+
  have pa1_disj_in2: "?\1 \ inside (?\2 \ ?\) = {}"
  proof (rule ccontr)
    assume ne: "?\1 \ inside (?\2 \ ?\) \ {}"
    have 1: "inside (?\ \ ?\2) \ ?\ = {}"
      by (metis (no_types) Diff_Int_distrib Diff_cancel inf_sup_absorb inf_sup_aci(3) inside_no_overlap)
    have 2: "outside (?\ \ ?\2) \ ?\ = {}"
      by (metis (no_types) Int_empty_right Int_left_commute inf_sup_absorb outside_no_overlap)
    have "path_image c1 \ outside (path_image c2 \ path_image c) = {}"
      using connectedD [OF co_c1, of "inside(?\2 \ ?\)" "outside(?\2 \ ?\)"]
        pa_c1 op_in2c op_out2c ne c1 c2c 1 2 by (auto simp: inf_sup_aci)
    then have "outside (?\2 \ ?\) \ outside (?\1 \ ?\2)"
      by (metis outside_Un_outside_Un sup_commute)
    with out_sub12
    have "outside(?\1 \ ?\2) = outside(?\2 \ ?\)" by blast
    then have "frontier(outside(?\1 \ ?\2)) = frontier(outside(?\2 \ ?\))"
      by simp
    then show False
      using inout_12 pi_disjoint c c1c c2c fr_out by auto
  qed
  have pa2_disj_in1: "?\2 \ inside(?\1 \ ?\) = {}"
  proof (rule ccontr)
    assume ne: "?\2 \ inside (?\1 \ ?\) \ {}"
    have 1: "inside (?\ \ ?\1) \ ?\ = {}"
      by (metis (no_types) Diff_Int_distrib Diff_cancel inf_sup_absorb inf_sup_aci(3) inside_no_overlap)
    have 2: "outside (?\ \ ?\1) \ ?\ = {}"
      by (metis (no_types) Int_empty_right Int_left_commute inf_sup_absorb outside_no_overlap)
    have "outside (?\1 \ ?\) \ outside (?\1 \ ?\2)"
      apply (rule outside_Un_outside_Un)
      using connectedD [OF co_c2, of "inside(?\1 \ ?\)" "outside(?\1 \ ?\)"]
        pa_c2 op_in1c op_out1c ne c2 c1c 1 2 by (auto simp: inf_sup_aci)
    with out_sub12
    have "outside(?\1 \ ?\2) = outside(?\1 \ ?\)"
      by blast
    then have "frontier(outside(?\1 \ ?\2)) = frontier(outside(?\1 \ ?\))"
      by simp
    then show False
      using inout_12 pi_disjoint c c1c c2c fr_out by auto
  qed
  have in_sub_in1: "inside(?\1 \ ?\) \ inside(?\1 \ ?\2)"
    using pa2_disj_in1 out_sub12 by (auto simp: inside_outside)
  have in_sub_in2: "inside(?\2 \ ?\) \ inside(?\1 \ ?\2)"
    using pa1_disj_in2 out_sub12 by (auto simp: inside_outside)
  have in_sub_out12: "inside(?\1 \ ?\) \ outside(?\2 \ ?\)"
  proof
    fix x
    assume x: "x \ inside (?\1 \ ?\)"
    then have xnot: "x \ ?\"
      by (simp add: inside_def)
    obtain z where zim: "z \ ?\1" and zout: "z \ outside(?\2 \ ?\)"
      unfolding outside_inside
      using nonempty_simple_path_endless [OF \<open>simple_path c1\<close>] c1 c1c c1c2 pa1_disj_in2 by auto
    obtain e where "e > 0" and e: "ball z e \ outside(?\2 \ ?\)"
      using zout op_out2c open_contains_ball_eq by blast
    have "z \ frontier (inside (?\1 \ ?\))"
      using zim by (auto simp: fr_in)
    then obtain w where w1: "w \ inside (?\1 \ ?\)" and dwz: "dist w z < e"
      using zim \<open>e > 0\<close> by (auto simp: frontier_def closure_approachable)
    then have w2: "w \ outside (?\2 \ ?\)"
      by (metis e dist_commute mem_ball subsetCE)
    then have "connected_component (- ?\2 \ - ?\) z w"
      unfolding connected_component_def
      by (metis co_out2c compl_sup inside_Un_outside sup_ge2 zout)
    moreover have "connected_component (- ?\2 \ - ?\) w x"
      unfolding connected_component_def
      using pa2_disj_in1 co_in1c x w1 union_with_outside by fastforce
    ultimately have eq: "connected_component_set (- ?\2 \ - ?\) x =
                         connected_component_set (- ?\<Theta>2 \<inter> - ?\<Theta>) z"
      by (metis (mono_tags, lifting) connected_component_eq mem_Collect_eq)
    show "x \ outside (?\2 \ ?\)"
      using zout x pa2_disj_in1 by (auto simp: outside_def eq xnot)
  qed
  have in_sub_out21: "inside(?\2 \ ?\) \ outside(?\1 \ ?\)"
  proof
    fix x
    assume x: "x \ inside (?\2 \ ?\)"
    then have xnot: "x \ ?\"
      by (simp add: inside_def)
    obtain z where zim: "z \ ?\2" and zout: "z \ outside(?\1 \ ?\)"
      unfolding outside_inside
      using nonempty_simple_path_endless [OF \<open>simple_path c2\<close>] c1c2 c2 c2c pa2_disj_in1 by auto
    obtain e where "e > 0" and e: "ball z e \ outside(?\1 \ ?\)"
      using zout op_out1c open_contains_ball_eq by blast
    have "z \ frontier (inside (?\2 \ ?\))"
      using zim by (auto simp: fr_in)
    then obtain w where w2: "w \ inside (?\2 \ ?\)" and dwz: "dist w z < e"
      using zim \<open>e > 0\<close> by (auto simp: frontier_def closure_approachable)
    then have w1: "w \ outside (?\1 \ ?\)"
      by (metis e dist_commute mem_ball subsetCE)
    then have "connected_component (- ?\1 \ - ?\) z w"
      unfolding connected_component_def
      by (metis Compl_Un co_out1c inside_Un_outside sup_ge2 zout)
    moreover have "connected_component (- ?\1 \ - ?\) w x"
      unfolding connected_component_def
      using pa1_disj_in2 co_in2c x w2 union_with_outside by fastforce
    ultimately have eq: "connected_component_set (- ?\1 \ - ?\) x =
                           connected_component_set (- ?\<Theta>1 \<inter> - ?\<Theta>) z"
      by (metis (no_types, lifting) connected_component_eq mem_Collect_eq)
    show "x \ outside (?\1 \ ?\)"
      using zout x pa1_disj_in2 by (auto simp: outside_def eq xnot)
  qed
  show ?thesis
  proof
    show "inside (?\1 \ ?\) \ inside (?\2 \ ?\) = {}"
      by (metis Int_Un_distrib in_sub_out12 bot_eq_sup_iff disjoint_eq_subset_Compl outside_inside)
    have *: "outside (?\1 \ ?\) \ outside (?\2 \ ?\) \ outside (?\1 \ ?\2)"
    proof (rule components_maximal)
      show out_in: "outside (?\1 \ ?\2) \ components (- (?\1 \ ?\2))"
        unfolding outside_in_components co_out12c
        using co_out12c fr_out(1) by force
      have conn_U: "connected (- (closure (inside (?\1 \ ?\)) \ closure (inside (?\2 \ ?\))))"
      proof (rule Janiszewski_connected, simp_all)
        show "bounded (inside (?\1 \ ?\))"
          by (simp add: \<open>simple_path c1\<close> \<open>simple_path c\<close> bounded_inside bounded_simple_path_image)
        have if1: "- (inside (?\1 \ ?\) \ frontier (inside (?\1 \ ?\))) = - ?\1 \ - ?\ \ - inside (?\1 \ ?\)"
          by (metis (no_types, lifting) Int_commute Jordan_inside_outside c c1 compl_sup path_image_join path_image_reversepath pathfinish_join pathfinish_reversepath pathstart_join pathstart_reversepath sp(2) closure_Un_frontier fr_out(3))
        then show "connected (- closure (inside (?\1 \ ?\)))"
          by (metis Compl_Un outside_inside co_out1c closure_Un_frontier)
        have if2: "- (inside (?\2 \ ?\) \ frontier (inside (?\2 \ ?\))) = - ?\2 \ - ?\ \ - inside (?\2 \ ?\)"
          by (metis (no_types, lifting) Int_commute Jordan_inside_outside c c2 compl_sup path_image_join path_image_reversepath pathfinish_join pathfinish_reversepath pathstart_join pathstart_reversepath sp(3) closure_Un_frontier fr_out(2))
        then show "connected (- closure (inside (?\2 \ ?\)))"
          by (metis Compl_Un outside_inside co_out2c closure_Un_frontier)
        have "connected(?\)"
          by (metis \<open>simple_path c\<close> connected_simple_path_image)
        moreover
        have "closure (inside (?\1 \ ?\)) \ closure (inside (?\2 \ ?\)) = ?\"
          (is "?lhs = ?rhs")
        proof
          show "?lhs \ ?rhs"
          proof clarify
            fix x
            assume x: "x \ closure (inside (?\1 \ ?\))" "x \ closure (inside (?\2 \ ?\))"
            then have "x \ inside (?\1 \ ?\)"
              by (meson closure_iff_nhds_not_empty in_sub_out12 inside_Int_outside op_in1c)
            with fr_in x show "x \ ?\"
              by (metis c1c c1c2 closure_Un_frontier pa1_disj_in2 Int_iff Un_iff insert_disjoint(2) insert_subset subsetI subset_antisym)
          qed
          show "?rhs \ ?lhs"
            using if1 if2 closure_Un_frontier by fastforce
        qed
        ultimately
        show "connected (closure (inside (?\1 \ ?\)) \ closure (inside (?\2 \ ?\)))"
          by auto
      qed
      show "connected (outside (?\1 \ ?\) \ outside (?\2 \ ?\))"
        using fr_in conn_U  by (simp add: closure_Un_frontier outside_inside Un_commute)
      show "outside (?\1 \ ?\) \ outside (?\2 \ ?\) \ - (?\1 \ ?\2)"
        by clarify (metis Diff_Compl Diff_iff Un_iff inf_sup_absorb outside_inside)
      show "outside (?\1 \ ?\2) \
            (outside (?\<Theta>1 \<union> ?\<Theta>) \<inter> outside (?\<Theta>2 \<union> ?\<Theta>)) \<noteq> {}"
        by (metis Int_assoc out_in inf.orderE out_sub12(1) out_sub12(2) outside_in_components)
    qed
    show "inside (?\1 \ ?\) \ inside (?\2 \ ?\) \ (?\ - {a, b}) = inside (?\1 \ ?\2)"
      (is "?lhs = ?rhs")
    proof
      have " path_image c - {a, b} \ inside (path_image c1 \ path_image c2)"
        using c1c c2c inside_outside pi_disjoint by fastforce
      then show "?lhs \ ?rhs"
        by (simp add: in_sub_in1 in_sub_in2)
      have "inside (?\1 \ ?\2) \ inside (?\1 \ ?\) \ inside (?\2 \ ?\) \ (?\)"
        using Compl_anti_mono [OF *] by (force simp: inside_outside)
      moreover have "inside (?\1 \ ?\2) \ -{a,b}"
        using c1 union_with_outside by fastforce
      ultimately show "?rhs \ ?lhs" by auto
    qed
  qed
qed

end

quality97%

¤ Dauer der Verarbeitung: 0.20 Sekunden (vorverarbeitet) ¤

*© Formatika GbR, Deutschland

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.