src/HOL/Analysis/Fashoda_Theorem.thy
 author wenzelm Sun Sep 18 20:33:48 2016 +0200 (2016-09-18) changeset 63915 bab633745c7f parent 63627 6ddb43c6b711 child 64267 b9a1486e79be permissions -rw-r--r--
tuned proofs;
```     1 (*  Author:     John Harrison
```
```     2     Author:     Robert Himmelmann, TU Muenchen (translation from HOL light)
```
```     3 *)
```
```     4
```
```     5 section \<open>Fashoda meet theorem\<close>
```
```     6
```
```     7 theory Fashoda_Theorem
```
```     8 imports Brouwer_Fixpoint Path_Connected Cartesian_Euclidean_Space
```
```     9 begin
```
```    10
```
```    11 subsection \<open>Bijections between intervals.\<close>
```
```    12
```
```    13 definition interval_bij :: "'a \<times> 'a \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<Rightarrow> 'a::euclidean_space"
```
```    14   where "interval_bij =
```
```    15     (\<lambda>(a, b) (u, v) x. (\<Sum>i\<in>Basis. (u\<bullet>i + (x\<bullet>i - a\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (v\<bullet>i - u\<bullet>i)) *\<^sub>R i))"
```
```    16
```
```    17 lemma interval_bij_affine:
```
```    18   "interval_bij (a,b) (u,v) = (\<lambda>x. (\<Sum>i\<in>Basis. ((v\<bullet>i - u\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (x\<bullet>i)) *\<^sub>R i) +
```
```    19     (\<Sum>i\<in>Basis. (u\<bullet>i - (v\<bullet>i - u\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (a\<bullet>i)) *\<^sub>R i))"
```
```    20   by (auto simp: setsum.distrib[symmetric] scaleR_add_left[symmetric] interval_bij_def fun_eq_iff
```
```    21     field_simps inner_simps add_divide_distrib[symmetric] intro!: setsum.cong)
```
```    22
```
```    23 lemma continuous_interval_bij:
```
```    24   fixes a b :: "'a::euclidean_space"
```
```    25   shows "continuous (at x) (interval_bij (a, b) (u, v))"
```
```    26   by (auto simp add: divide_inverse interval_bij_def intro!: continuous_setsum continuous_intros)
```
```    27
```
```    28 lemma continuous_on_interval_bij: "continuous_on s (interval_bij (a, b) (u, v))"
```
```    29   apply(rule continuous_at_imp_continuous_on)
```
```    30   apply (rule, rule continuous_interval_bij)
```
```    31   done
```
```    32
```
```    33 lemma in_interval_interval_bij:
```
```    34   fixes a b u v x :: "'a::euclidean_space"
```
```    35   assumes "x \<in> cbox a b"
```
```    36     and "cbox u v \<noteq> {}"
```
```    37   shows "interval_bij (a, b) (u, v) x \<in> cbox u v"
```
```    38   apply (simp only: interval_bij_def split_conv mem_box inner_setsum_left_Basis cong: ball_cong)
```
```    39   apply safe
```
```    40 proof -
```
```    41   fix i :: 'a
```
```    42   assume i: "i \<in> Basis"
```
```    43   have "cbox a b \<noteq> {}"
```
```    44     using assms by auto
```
```    45   with i have *: "a\<bullet>i \<le> b\<bullet>i" "u\<bullet>i \<le> v\<bullet>i"
```
```    46     using assms(2) by (auto simp add: box_eq_empty)
```
```    47   have x: "a\<bullet>i\<le>x\<bullet>i" "x\<bullet>i\<le>b\<bullet>i"
```
```    48     using assms(1)[unfolded mem_box] using i by auto
```
```    49   have "0 \<le> (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i)"
```
```    50     using * x by auto
```
```    51   then show "u \<bullet> i \<le> u \<bullet> i + (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i)"
```
```    52     using * by auto
```
```    53   have "((x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i)) * (v \<bullet> i - u \<bullet> i) \<le> 1 * (v \<bullet> i - u \<bullet> i)"
```
```    54     apply (rule mult_right_mono)
```
```    55     unfolding divide_le_eq_1
```
```    56     using * x
```
```    57     apply auto
```
```    58     done
```
```    59   then show "u \<bullet> i + (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i) \<le> v \<bullet> i"
```
```    60     using * by auto
```
```    61 qed
```
```    62
```
```    63 lemma interval_bij_bij:
```
```    64   "\<forall>(i::'a::euclidean_space)\<in>Basis. a\<bullet>i < b\<bullet>i \<and> u\<bullet>i < v\<bullet>i \<Longrightarrow>
```
```    65     interval_bij (a, b) (u, v) (interval_bij (u, v) (a, b) x) = x"
```
```    66   by (auto simp: interval_bij_def euclidean_eq_iff[where 'a='a])
```
```    67
```
```    68 lemma interval_bij_bij_cart: fixes x::"real^'n" assumes "\<forall>i. a\$i < b\$i \<and> u\$i < v\$i"
```
```    69   shows "interval_bij (a,b) (u,v) (interval_bij (u,v) (a,b) x) = x"
```
```    70   using assms by (intro interval_bij_bij) (auto simp: Basis_vec_def inner_axis)
```
```    71
```
```    72
```
```    73 subsection \<open>Fashoda meet theorem\<close>
```
```    74
```
```    75 lemma infnorm_2:
```
```    76   fixes x :: "real^2"
```
```    77   shows "infnorm x = max \<bar>x\$1\<bar> \<bar>x\$2\<bar>"
```
```    78   unfolding infnorm_cart UNIV_2 by (rule cSup_eq) auto
```
```    79
```
```    80 lemma infnorm_eq_1_2:
```
```    81   fixes x :: "real^2"
```
```    82   shows "infnorm x = 1 \<longleftrightarrow>
```
```    83     \<bar>x\$1\<bar> \<le> 1 \<and> \<bar>x\$2\<bar> \<le> 1 \<and> (x\$1 = -1 \<or> x\$1 = 1 \<or> x\$2 = -1 \<or> x\$2 = 1)"
```
```    84   unfolding infnorm_2 by auto
```
```    85
```
```    86 lemma infnorm_eq_1_imp:
```
```    87   fixes x :: "real^2"
```
```    88   assumes "infnorm x = 1"
```
```    89   shows "\<bar>x\$1\<bar> \<le> 1" and "\<bar>x\$2\<bar> \<le> 1"
```
```    90   using assms unfolding infnorm_eq_1_2 by auto
```
```    91
```
```    92 lemma fashoda_unit:
```
```    93   fixes f g :: "real \<Rightarrow> real^2"
```
```    94   assumes "f ` {-1 .. 1} \<subseteq> cbox (-1) 1"
```
```    95     and "g ` {-1 .. 1} \<subseteq> cbox (-1) 1"
```
```    96     and "continuous_on {-1 .. 1} f"
```
```    97     and "continuous_on {-1 .. 1} g"
```
```    98     and "f (- 1)\$1 = - 1"
```
```    99     and "f 1\$1 = 1" "g (- 1) \$2 = -1"
```
```   100     and "g 1 \$2 = 1"
```
```   101   shows "\<exists>s\<in>{-1 .. 1}. \<exists>t\<in>{-1 .. 1}. f s = g t"
```
```   102 proof (rule ccontr)
```
```   103   assume "\<not> ?thesis"
```
```   104   note as = this[unfolded bex_simps,rule_format]
```
```   105   define sqprojection
```
```   106     where [abs_def]: "sqprojection z = (inverse (infnorm z)) *\<^sub>R z" for z :: "real^2"
```
```   107   define negatex :: "real^2 \<Rightarrow> real^2"
```
```   108     where "negatex x = (vector [-(x\$1), x\$2])" for x
```
```   109   have lem1: "\<forall>z::real^2. infnorm (negatex z) = infnorm z"
```
```   110     unfolding negatex_def infnorm_2 vector_2 by auto
```
```   111   have lem2: "\<forall>z. z \<noteq> 0 \<longrightarrow> infnorm (sqprojection z) = 1"
```
```   112     unfolding sqprojection_def
```
```   113     unfolding infnorm_mul[unfolded scalar_mult_eq_scaleR]
```
```   114     unfolding abs_inverse real_abs_infnorm
```
```   115     apply (subst infnorm_eq_0[symmetric])
```
```   116     apply auto
```
```   117     done
```
```   118   let ?F = "\<lambda>w::real^2. (f \<circ> (\<lambda>x. x\$1)) w - (g \<circ> (\<lambda>x. x\$2)) w"
```
```   119   have *: "\<And>i. (\<lambda>x::real^2. x \$ i) ` cbox (- 1) 1 = {-1 .. 1}"
```
```   120     apply (rule set_eqI)
```
```   121     unfolding image_iff Bex_def mem_interval_cart interval_cbox_cart
```
```   122     apply rule
```
```   123     defer
```
```   124     apply (rule_tac x="vec x" in exI)
```
```   125     apply auto
```
```   126     done
```
```   127   {
```
```   128     fix x
```
```   129     assume "x \<in> (\<lambda>w. (f \<circ> (\<lambda>x. x \$ 1)) w - (g \<circ> (\<lambda>x. x \$ 2)) w) ` (cbox (- 1) (1::real^2))"
```
```   130     then obtain w :: "real^2" where w:
```
```   131         "w \<in> cbox (- 1) 1"
```
```   132         "x = (f \<circ> (\<lambda>x. x \$ 1)) w - (g \<circ> (\<lambda>x. x \$ 2)) w"
```
```   133       unfolding image_iff ..
```
```   134     then have "x \<noteq> 0"
```
```   135       using as[of "w\$1" "w\$2"]
```
```   136       unfolding mem_interval_cart atLeastAtMost_iff
```
```   137       by auto
```
```   138   } note x0 = this
```
```   139   have 21: "\<And>i::2. i \<noteq> 1 \<Longrightarrow> i = 2"
```
```   140     using UNIV_2 by auto
```
```   141   have 1: "box (- 1) (1::real^2) \<noteq> {}"
```
```   142     unfolding interval_eq_empty_cart by auto
```
```   143   have 2: "continuous_on (cbox (- 1) 1) (negatex \<circ> sqprojection \<circ> ?F)"
```
```   144     apply (intro continuous_intros continuous_on_component)
```
```   145     unfolding *
```
```   146     apply (rule assms)+
```
```   147     apply (subst sqprojection_def)
```
```   148     apply (intro continuous_intros)
```
```   149     apply (simp add: infnorm_eq_0 x0)
```
```   150     apply (rule linear_continuous_on)
```
```   151   proof -
```
```   152     show "bounded_linear negatex"
```
```   153       apply (rule bounded_linearI')
```
```   154       unfolding vec_eq_iff
```
```   155     proof (rule_tac[!] allI)
```
```   156       fix i :: 2
```
```   157       fix x y :: "real^2"
```
```   158       fix c :: real
```
```   159       show "negatex (x + y) \$ i =
```
```   160         (negatex x + negatex y) \$ i" "negatex (c *\<^sub>R x) \$ i = (c *\<^sub>R negatex x) \$ i"
```
```   161         apply -
```
```   162         apply (case_tac[!] "i\<noteq>1")
```
```   163         prefer 3
```
```   164         apply (drule_tac[1-2] 21)
```
```   165         unfolding negatex_def
```
```   166         apply (auto simp add:vector_2)
```
```   167         done
```
```   168     qed
```
```   169   qed
```
```   170   have 3: "(negatex \<circ> sqprojection \<circ> ?F) ` cbox (-1) 1 \<subseteq> cbox (-1) 1"
```
```   171     unfolding subset_eq
```
```   172   proof (rule, goal_cases)
```
```   173     case (1 x)
```
```   174     then obtain y :: "real^2" where y:
```
```   175         "y \<in> cbox (- 1) 1"
```
```   176         "x = (negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x \$ 1)) w - (g \<circ> (\<lambda>x. x \$ 2)) w)) y"
```
```   177       unfolding image_iff ..
```
```   178     have "?F y \<noteq> 0"
```
```   179       apply (rule x0)
```
```   180       using y(1)
```
```   181       apply auto
```
```   182       done
```
```   183     then have *: "infnorm (sqprojection (?F y)) = 1"
```
```   184       unfolding y o_def
```
```   185       by - (rule lem2[rule_format])
```
```   186     have "infnorm x = 1"
```
```   187       unfolding *[symmetric] y o_def
```
```   188       by (rule lem1[rule_format])
```
```   189     then show "x \<in> cbox (-1) 1"
```
```   190       unfolding mem_interval_cart interval_cbox_cart infnorm_2
```
```   191       apply -
```
```   192       apply rule
```
```   193     proof -
```
```   194       fix i
```
```   195       assume "max \<bar>x \$ 1\<bar> \<bar>x \$ 2\<bar> = 1"
```
```   196       then show "(- 1) \$ i \<le> x \$ i \<and> x \$ i \<le> 1 \$ i"
```
```   197         apply (cases "i = 1")
```
```   198         defer
```
```   199         apply (drule 21)
```
```   200         apply auto
```
```   201         done
```
```   202     qed
```
```   203   qed
```
```   204   obtain x :: "real^2" where x:
```
```   205       "x \<in> cbox (- 1) 1"
```
```   206       "(negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x \$ 1)) w - (g \<circ> (\<lambda>x. x \$ 2)) w)) x = x"
```
```   207     apply (rule brouwer_weak[of "cbox (- 1) (1::real^2)" "negatex \<circ> sqprojection \<circ> ?F"])
```
```   208     apply (rule compact_cbox convex_box)+
```
```   209     unfolding interior_cbox
```
```   210     apply (rule 1 2 3)+
```
```   211     apply blast
```
```   212     done
```
```   213   have "?F x \<noteq> 0"
```
```   214     apply (rule x0)
```
```   215     using x(1)
```
```   216     apply auto
```
```   217     done
```
```   218   then have *: "infnorm (sqprojection (?F x)) = 1"
```
```   219     unfolding o_def
```
```   220     by (rule lem2[rule_format])
```
```   221   have nx: "infnorm x = 1"
```
```   222     apply (subst x(2)[symmetric])
```
```   223     unfolding *[symmetric] o_def
```
```   224     apply (rule lem1[rule_format])
```
```   225     done
```
```   226   have "\<forall>x i. x \<noteq> 0 \<longrightarrow> (0 < (sqprojection x)\$i \<longleftrightarrow> 0 < x\$i)"
```
```   227     and "\<forall>x i. x \<noteq> 0 \<longrightarrow> ((sqprojection x)\$i < 0 \<longleftrightarrow> x\$i < 0)"
```
```   228     apply -
```
```   229     apply (rule_tac[!] allI impI)+
```
```   230   proof -
```
```   231     fix x :: "real^2"
```
```   232     fix i :: 2
```
```   233     assume x: "x \<noteq> 0"
```
```   234     have "inverse (infnorm x) > 0"
```
```   235       using x[unfolded infnorm_pos_lt[symmetric]] by auto
```
```   236     then show "(0 < sqprojection x \$ i) = (0 < x \$ i)"
```
```   237       and "(sqprojection x \$ i < 0) = (x \$ i < 0)"
```
```   238       unfolding sqprojection_def vector_component_simps vector_scaleR_component real_scaleR_def
```
```   239       unfolding zero_less_mult_iff mult_less_0_iff
```
```   240       by (auto simp add: field_simps)
```
```   241   qed
```
```   242   note lem3 = this[rule_format]
```
```   243   have x1: "x \$ 1 \<in> {- 1..1::real}" "x \$ 2 \<in> {- 1..1::real}"
```
```   244     using x(1) unfolding mem_interval_cart by auto
```
```   245   then have nz: "f (x \$ 1) - g (x \$ 2) \<noteq> 0"
```
```   246     unfolding right_minus_eq
```
```   247     apply -
```
```   248     apply (rule as)
```
```   249     apply auto
```
```   250     done
```
```   251   have "x \$ 1 = -1 \<or> x \$ 1 = 1 \<or> x \$ 2 = -1 \<or> x \$ 2 = 1"
```
```   252     using nx unfolding infnorm_eq_1_2 by auto
```
```   253   then show False
```
```   254   proof -
```
```   255     fix P Q R S
```
```   256     presume "P \<or> Q \<or> R \<or> S"
```
```   257       and "P \<Longrightarrow> False"
```
```   258       and "Q \<Longrightarrow> False"
```
```   259       and "R \<Longrightarrow> False"
```
```   260       and "S \<Longrightarrow> False"
```
```   261     then show False by auto
```
```   262   next
```
```   263     assume as: "x\$1 = 1"
```
```   264     then have *: "f (x \$ 1) \$ 1 = 1"
```
```   265       using assms(6) by auto
```
```   266     have "sqprojection (f (x\$1) - g (x\$2)) \$ 1 < 0"
```
```   267       using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]]
```
```   268       unfolding as negatex_def vector_2
```
```   269       by auto
```
```   270     moreover
```
```   271     from x1 have "g (x \$ 2) \<in> cbox (-1) 1"
```
```   272       apply -
```
```   273       apply (rule assms(2)[unfolded subset_eq,rule_format])
```
```   274       apply auto
```
```   275       done
```
```   276     ultimately show False
```
```   277       unfolding lem3[OF nz] vector_component_simps * mem_interval_cart
```
```   278       apply (erule_tac x=1 in allE)
```
```   279       apply auto
```
```   280       done
```
```   281   next
```
```   282     assume as: "x\$1 = -1"
```
```   283     then have *: "f (x \$ 1) \$ 1 = - 1"
```
```   284       using assms(5) by auto
```
```   285     have "sqprojection (f (x\$1) - g (x\$2)) \$ 1 > 0"
```
```   286       using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]]
```
```   287       unfolding as negatex_def vector_2
```
```   288       by auto
```
```   289     moreover
```
```   290     from x1 have "g (x \$ 2) \<in> cbox (-1) 1"
```
```   291       apply -
```
```   292       apply (rule assms(2)[unfolded subset_eq,rule_format])
```
```   293       apply auto
```
```   294       done
```
```   295     ultimately show False
```
```   296       unfolding lem3[OF nz] vector_component_simps * mem_interval_cart
```
```   297       apply (erule_tac x=1 in allE)
```
```   298       apply auto
```
```   299       done
```
```   300   next
```
```   301     assume as: "x\$2 = 1"
```
```   302     then have *: "g (x \$ 2) \$ 2 = 1"
```
```   303       using assms(8) by auto
```
```   304     have "sqprojection (f (x\$1) - g (x\$2)) \$ 2 > 0"
```
```   305       using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]]
```
```   306       unfolding as negatex_def vector_2
```
```   307       by auto
```
```   308     moreover
```
```   309     from x1 have "f (x \$ 1) \<in> cbox (-1) 1"
```
```   310       apply -
```
```   311       apply (rule assms(1)[unfolded subset_eq,rule_format])
```
```   312       apply auto
```
```   313       done
```
```   314     ultimately show False
```
```   315       unfolding lem3[OF nz] vector_component_simps * mem_interval_cart
```
```   316       apply (erule_tac x=2 in allE)
```
```   317       apply auto
```
```   318       done
```
```   319   next
```
```   320     assume as: "x\$2 = -1"
```
```   321     then have *: "g (x \$ 2) \$ 2 = - 1"
```
```   322       using assms(7) by auto
```
```   323     have "sqprojection (f (x\$1) - g (x\$2)) \$ 2 < 0"
```
```   324       using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]]
```
```   325       unfolding as negatex_def vector_2
```
```   326       by auto
```
```   327     moreover
```
```   328     from x1 have "f (x \$ 1) \<in> cbox (-1) 1"
```
```   329       apply -
```
```   330       apply (rule assms(1)[unfolded subset_eq,rule_format])
```
```   331       apply auto
```
```   332       done
```
```   333     ultimately show False
```
```   334       unfolding lem3[OF nz] vector_component_simps * mem_interval_cart
```
```   335       apply (erule_tac x=2 in allE)
```
```   336       apply auto
```
```   337       done
```
```   338   qed auto
```
```   339 qed
```
```   340
```
```   341 lemma fashoda_unit_path:
```
```   342   fixes f g :: "real \<Rightarrow> real^2"
```
```   343   assumes "path f"
```
```   344     and "path g"
```
```   345     and "path_image f \<subseteq> cbox (-1) 1"
```
```   346     and "path_image g \<subseteq> cbox (-1) 1"
```
```   347     and "(pathstart f)\$1 = -1"
```
```   348     and "(pathfinish f)\$1 = 1"
```
```   349     and "(pathstart g)\$2 = -1"
```
```   350     and "(pathfinish g)\$2 = 1"
```
```   351   obtains z where "z \<in> path_image f" and "z \<in> path_image g"
```
```   352 proof -
```
```   353   note assms=assms[unfolded path_def pathstart_def pathfinish_def path_image_def]
```
```   354   define iscale where [abs_def]: "iscale z = inverse 2 *\<^sub>R (z + 1)" for z :: real
```
```   355   have isc: "iscale ` {- 1..1} \<subseteq> {0..1}"
```
```   356     unfolding iscale_def by auto
```
```   357   have "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. (f \<circ> iscale) s = (g \<circ> iscale) t"
```
```   358   proof (rule fashoda_unit)
```
```   359     show "(f \<circ> iscale) ` {- 1..1} \<subseteq> cbox (- 1) 1" "(g \<circ> iscale) ` {- 1..1} \<subseteq> cbox (- 1) 1"
```
```   360       using isc and assms(3-4) by (auto simp add: image_comp [symmetric])
```
```   361     have *: "continuous_on {- 1..1} iscale"
```
```   362       unfolding iscale_def by (rule continuous_intros)+
```
```   363     show "continuous_on {- 1..1} (f \<circ> iscale)" "continuous_on {- 1..1} (g \<circ> iscale)"
```
```   364       apply -
```
```   365       apply (rule_tac[!] continuous_on_compose[OF *])
```
```   366       apply (rule_tac[!] continuous_on_subset[OF _ isc])
```
```   367       apply (rule assms)+
```
```   368       done
```
```   369     have *: "(1 / 2) *\<^sub>R (1 + (1::real^1)) = 1"
```
```   370       unfolding vec_eq_iff by auto
```
```   371     show "(f \<circ> iscale) (- 1) \$ 1 = - 1"
```
```   372       and "(f \<circ> iscale) 1 \$ 1 = 1"
```
```   373       and "(g \<circ> iscale) (- 1) \$ 2 = -1"
```
```   374       and "(g \<circ> iscale) 1 \$ 2 = 1"
```
```   375       unfolding o_def iscale_def
```
```   376       using assms
```
```   377       by (auto simp add: *)
```
```   378   qed
```
```   379   then obtain s t where st:
```
```   380       "s \<in> {- 1..1}"
```
```   381       "t \<in> {- 1..1}"
```
```   382       "(f \<circ> iscale) s = (g \<circ> iscale) t"
```
```   383     by auto
```
```   384   show thesis
```
```   385     apply (rule_tac z = "f (iscale s)" in that)
```
```   386     using st
```
```   387     unfolding o_def path_image_def image_iff
```
```   388     apply -
```
```   389     apply (rule_tac x="iscale s" in bexI)
```
```   390     prefer 3
```
```   391     apply (rule_tac x="iscale t" in bexI)
```
```   392     using isc[unfolded subset_eq, rule_format]
```
```   393     apply auto
```
```   394     done
```
```   395 qed
```
```   396
```
```   397 lemma fashoda:
```
```   398   fixes b :: "real^2"
```
```   399   assumes "path f"
```
```   400     and "path g"
```
```   401     and "path_image f \<subseteq> cbox a b"
```
```   402     and "path_image g \<subseteq> cbox a b"
```
```   403     and "(pathstart f)\$1 = a\$1"
```
```   404     and "(pathfinish f)\$1 = b\$1"
```
```   405     and "(pathstart g)\$2 = a\$2"
```
```   406     and "(pathfinish g)\$2 = b\$2"
```
```   407   obtains z where "z \<in> path_image f" and "z \<in> path_image g"
```
```   408 proof -
```
```   409   fix P Q S
```
```   410   presume "P \<or> Q \<or> S" "P \<Longrightarrow> thesis" and "Q \<Longrightarrow> thesis" and "S \<Longrightarrow> thesis"
```
```   411   then show thesis
```
```   412     by auto
```
```   413 next
```
```   414   have "cbox a b \<noteq> {}"
```
```   415     using assms(3) using path_image_nonempty[of f] by auto
```
```   416   then have "a \<le> b"
```
```   417     unfolding interval_eq_empty_cart less_eq_vec_def by (auto simp add: not_less)
```
```   418   then show "a\$1 = b\$1 \<or> a\$2 = b\$2 \<or> (a\$1 < b\$1 \<and> a\$2 < b\$2)"
```
```   419     unfolding less_eq_vec_def forall_2 by auto
```
```   420 next
```
```   421   assume as: "a\$1 = b\$1"
```
```   422   have "\<exists>z\<in>path_image g. z\$2 = (pathstart f)\$2"
```
```   423     apply (rule connected_ivt_component_cart)
```
```   424     apply (rule connected_path_image assms)+
```
```   425     apply (rule pathstart_in_path_image)
```
```   426     apply (rule pathfinish_in_path_image)
```
```   427     unfolding assms using assms(3)[unfolded path_image_def subset_eq,rule_format,of "f 0"]
```
```   428     unfolding pathstart_def
```
```   429     apply (auto simp add: less_eq_vec_def mem_interval_cart)
```
```   430     done
```
```   431   then obtain z :: "real^2" where z: "z \<in> path_image g" "z \$ 2 = pathstart f \$ 2" ..
```
```   432   have "z \<in> cbox a b"
```
```   433     using z(1) assms(4)
```
```   434     unfolding path_image_def
```
```   435     by blast
```
```   436   then have "z = f 0"
```
```   437     unfolding vec_eq_iff forall_2
```
```   438     unfolding z(2) pathstart_def
```
```   439     using assms(3)[unfolded path_image_def subset_eq mem_interval_cart,rule_format,of "f 0" 1]
```
```   440     unfolding mem_interval_cart
```
```   441     apply (erule_tac x=1 in allE)
```
```   442     using as
```
```   443     apply auto
```
```   444     done
```
```   445   then show thesis
```
```   446     apply -
```
```   447     apply (rule that[OF _ z(1)])
```
```   448     unfolding path_image_def
```
```   449     apply auto
```
```   450     done
```
```   451 next
```
```   452   assume as: "a\$2 = b\$2"
```
```   453   have "\<exists>z\<in>path_image f. z\$1 = (pathstart g)\$1"
```
```   454     apply (rule connected_ivt_component_cart)
```
```   455     apply (rule connected_path_image assms)+
```
```   456     apply (rule pathstart_in_path_image)
```
```   457     apply (rule pathfinish_in_path_image)
```
```   458     unfolding assms
```
```   459     using assms(4)[unfolded path_image_def subset_eq,rule_format,of "g 0"]
```
```   460     unfolding pathstart_def
```
```   461     apply (auto simp add: less_eq_vec_def mem_interval_cart)
```
```   462     done
```
```   463   then obtain z where z: "z \<in> path_image f" "z \$ 1 = pathstart g \$ 1" ..
```
```   464   have "z \<in> cbox a b"
```
```   465     using z(1) assms(3)
```
```   466     unfolding path_image_def
```
```   467     by blast
```
```   468   then have "z = g 0"
```
```   469     unfolding vec_eq_iff forall_2
```
```   470     unfolding z(2) pathstart_def
```
```   471     using assms(4)[unfolded path_image_def subset_eq mem_interval_cart,rule_format,of "g 0" 2]
```
```   472     unfolding mem_interval_cart
```
```   473     apply (erule_tac x=2 in allE)
```
```   474     using as
```
```   475     apply auto
```
```   476     done
```
```   477   then show thesis
```
```   478     apply -
```
```   479     apply (rule that[OF z(1)])
```
```   480     unfolding path_image_def
```
```   481     apply auto
```
```   482     done
```
```   483 next
```
```   484   assume as: "a \$ 1 < b \$ 1 \<and> a \$ 2 < b \$ 2"
```
```   485   have int_nem: "cbox (-1) (1::real^2) \<noteq> {}"
```
```   486     unfolding interval_eq_empty_cart by auto
```
```   487   obtain z :: "real^2" where z:
```
```   488       "z \<in> (interval_bij (a, b) (- 1, 1) \<circ> f) ` {0..1}"
```
```   489       "z \<in> (interval_bij (a, b) (- 1, 1) \<circ> g) ` {0..1}"
```
```   490     apply (rule fashoda_unit_path[of "interval_bij (a,b) (- 1,1) \<circ> f" "interval_bij (a,b) (- 1,1) \<circ> g"])
```
```   491     unfolding path_def path_image_def pathstart_def pathfinish_def
```
```   492     apply (rule_tac[1-2] continuous_on_compose)
```
```   493     apply (rule assms[unfolded path_def] continuous_on_interval_bij)+
```
```   494     unfolding subset_eq
```
```   495     apply(rule_tac[1-2] ballI)
```
```   496   proof -
```
```   497     fix x
```
```   498     assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> f) ` {0..1}"
```
```   499     then obtain y where y:
```
```   500         "y \<in> {0..1}"
```
```   501         "x = (interval_bij (a, b) (- 1, 1) \<circ> f) y"
```
```   502       unfolding image_iff ..
```
```   503     show "x \<in> cbox (- 1) 1"
```
```   504       unfolding y o_def
```
```   505       apply (rule in_interval_interval_bij)
```
```   506       using y(1)
```
```   507       using assms(3)[unfolded path_image_def subset_eq] int_nem
```
```   508       apply auto
```
```   509       done
```
```   510   next
```
```   511     fix x
```
```   512     assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> g) ` {0..1}"
```
```   513     then obtain y where y:
```
```   514         "y \<in> {0..1}"
```
```   515         "x = (interval_bij (a, b) (- 1, 1) \<circ> g) y"
```
```   516       unfolding image_iff ..
```
```   517     show "x \<in> cbox (- 1) 1"
```
```   518       unfolding y o_def
```
```   519       apply (rule in_interval_interval_bij)
```
```   520       using y(1)
```
```   521       using assms(4)[unfolded path_image_def subset_eq] int_nem
```
```   522       apply auto
```
```   523       done
```
```   524   next
```
```   525     show "(interval_bij (a, b) (- 1, 1) \<circ> f) 0 \$ 1 = -1"
```
```   526       and "(interval_bij (a, b) (- 1, 1) \<circ> f) 1 \$ 1 = 1"
```
```   527       and "(interval_bij (a, b) (- 1, 1) \<circ> g) 0 \$ 2 = -1"
```
```   528       and "(interval_bij (a, b) (- 1, 1) \<circ> g) 1 \$ 2 = 1"
```
```   529       using assms as
```
```   530       by (simp_all add: axis_in_Basis cart_eq_inner_axis pathstart_def pathfinish_def interval_bij_def)
```
```   531          (simp_all add: inner_axis)
```
```   532   qed
```
```   533   from z(1) obtain zf where zf:
```
```   534       "zf \<in> {0..1}"
```
```   535       "z = (interval_bij (a, b) (- 1, 1) \<circ> f) zf"
```
```   536     unfolding image_iff ..
```
```   537   from z(2) obtain zg where zg:
```
```   538       "zg \<in> {0..1}"
```
```   539       "z = (interval_bij (a, b) (- 1, 1) \<circ> g) zg"
```
```   540     unfolding image_iff ..
```
```   541   have *: "\<forall>i. (- 1) \$ i < (1::real^2) \$ i \<and> a \$ i < b \$ i"
```
```   542     unfolding forall_2
```
```   543     using as
```
```   544     by auto
```
```   545   show thesis
```
```   546     apply (rule_tac z="interval_bij (- 1,1) (a,b) z" in that)
```
```   547     apply (subst zf)
```
```   548     defer
```
```   549     apply (subst zg)
```
```   550     unfolding o_def interval_bij_bij_cart[OF *] path_image_def
```
```   551     using zf(1) zg(1)
```
```   552     apply auto
```
```   553     done
```
```   554 qed
```
```   555
```
```   556
```
```   557 subsection \<open>Some slightly ad hoc lemmas I use below\<close>
```
```   558
```
```   559 lemma segment_vertical:
```
```   560   fixes a :: "real^2"
```
```   561   assumes "a\$1 = b\$1"
```
```   562   shows "x \<in> closed_segment a b \<longleftrightarrow>
```
```   563     x\$1 = a\$1 \<and> x\$1 = b\$1 \<and> (a\$2 \<le> x\$2 \<and> x\$2 \<le> b\$2 \<or> b\$2 \<le> x\$2 \<and> x\$2 \<le> a\$2)"
```
```   564   (is "_ = ?R")
```
```   565 proof -
```
```   566   let ?L = "\<exists>u. (x \$ 1 = (1 - u) * a \$ 1 + u * b \$ 1 \<and> x \$ 2 = (1 - u) * a \$ 2 + u * b \$ 2) \<and> 0 \<le> u \<and> u \<le> 1"
```
```   567   {
```
```   568     presume "?L \<Longrightarrow> ?R" and "?R \<Longrightarrow> ?L"
```
```   569     then show ?thesis
```
```   570       unfolding closed_segment_def mem_Collect_eq
```
```   571       unfolding vec_eq_iff forall_2 scalar_mult_eq_scaleR[symmetric] vector_component_simps
```
```   572       by blast
```
```   573   }
```
```   574   {
```
```   575     assume ?L
```
```   576     then obtain u where u:
```
```   577         "x \$ 1 = (1 - u) * a \$ 1 + u * b \$ 1"
```
```   578         "x \$ 2 = (1 - u) * a \$ 2 + u * b \$ 2"
```
```   579         "0 \<le> u"
```
```   580         "u \<le> 1"
```
```   581       by blast
```
```   582     { fix b a
```
```   583       assume "b + u * a > a + u * b"
```
```   584       then have "(1 - u) * b > (1 - u) * a"
```
```   585         by (auto simp add:field_simps)
```
```   586       then have "b \<ge> a"
```
```   587         apply (drule_tac mult_left_less_imp_less)
```
```   588         using u
```
```   589         apply auto
```
```   590         done
```
```   591       then have "u * a \<le> u * b"
```
```   592         apply -
```
```   593         apply (rule mult_left_mono[OF _ u(3)])
```
```   594         using u(3-4)
```
```   595         apply (auto simp add: field_simps)
```
```   596         done
```
```   597     } note * = this
```
```   598     {
```
```   599       fix a b
```
```   600       assume "u * b > u * a"
```
```   601       then have "(1 - u) * a \<le> (1 - u) * b"
```
```   602         apply -
```
```   603         apply (rule mult_left_mono)
```
```   604         apply (drule mult_left_less_imp_less)
```
```   605         using u
```
```   606         apply auto
```
```   607         done
```
```   608       then have "a + u * b \<le> b + u * a"
```
```   609         by (auto simp add: field_simps)
```
```   610     } note ** = this
```
```   611     then show ?R
```
```   612       unfolding u assms
```
```   613       using u
```
```   614       by (auto simp add:field_simps not_le intro: * **)
```
```   615   }
```
```   616   {
```
```   617     assume ?R
```
```   618     then show ?L
```
```   619     proof (cases "x\$2 = b\$2")
```
```   620       case True
```
```   621       then show ?L
```
```   622         apply (rule_tac x="(x\$2 - a\$2) / (b\$2 - a\$2)" in exI)
```
```   623         unfolding assms True
```
```   624         using \<open>?R\<close>
```
```   625         apply (auto simp add: field_simps)
```
```   626         done
```
```   627     next
```
```   628       case False
```
```   629       then show ?L
```
```   630         apply (rule_tac x="1 - (x\$2 - b\$2) / (a\$2 - b\$2)" in exI)
```
```   631         unfolding assms
```
```   632         using \<open>?R\<close>
```
```   633         apply (auto simp add: field_simps)
```
```   634         done
```
```   635     qed
```
```   636   }
```
```   637 qed
```
```   638
```
```   639 lemma segment_horizontal:
```
```   640   fixes a :: "real^2"
```
```   641   assumes "a\$2 = b\$2"
```
```   642   shows "x \<in> closed_segment a b \<longleftrightarrow>
```
```   643     x\$2 = a\$2 \<and> x\$2 = b\$2 \<and> (a\$1 \<le> x\$1 \<and> x\$1 \<le> b\$1 \<or> b\$1 \<le> x\$1 \<and> x\$1 \<le> a\$1)"
```
```   644   (is "_ = ?R")
```
```   645 proof -
```
```   646   let ?L = "\<exists>u. (x \$ 1 = (1 - u) * a \$ 1 + u * b \$ 1 \<and> x \$ 2 = (1 - u) * a \$ 2 + u * b \$ 2) \<and> 0 \<le> u \<and> u \<le> 1"
```
```   647   {
```
```   648     presume "?L \<Longrightarrow> ?R" and "?R \<Longrightarrow> ?L"
```
```   649     then show ?thesis
```
```   650       unfolding closed_segment_def mem_Collect_eq
```
```   651       unfolding vec_eq_iff forall_2 scalar_mult_eq_scaleR[symmetric] vector_component_simps
```
```   652       by blast
```
```   653   }
```
```   654   {
```
```   655     assume ?L
```
```   656     then obtain u where u:
```
```   657         "x \$ 1 = (1 - u) * a \$ 1 + u * b \$ 1"
```
```   658         "x \$ 2 = (1 - u) * a \$ 2 + u * b \$ 2"
```
```   659         "0 \<le> u"
```
```   660         "u \<le> 1"
```
```   661       by blast
```
```   662     {
```
```   663       fix b a
```
```   664       assume "b + u * a > a + u * b"
```
```   665       then have "(1 - u) * b > (1 - u) * a"
```
```   666         by (auto simp add: field_simps)
```
```   667       then have "b \<ge> a"
```
```   668         apply (drule_tac mult_left_less_imp_less)
```
```   669         using u
```
```   670         apply auto
```
```   671         done
```
```   672       then have "u * a \<le> u * b"
```
```   673         apply -
```
```   674         apply (rule mult_left_mono[OF _ u(3)])
```
```   675         using u(3-4)
```
```   676         apply (auto simp add: field_simps)
```
```   677         done
```
```   678     } note * = this
```
```   679     {
```
```   680       fix a b
```
```   681       assume "u * b > u * a"
```
```   682       then have "(1 - u) * a \<le> (1 - u) * b"
```
```   683         apply -
```
```   684         apply (rule mult_left_mono)
```
```   685         apply (drule mult_left_less_imp_less)
```
```   686         using u
```
```   687         apply auto
```
```   688         done
```
```   689       then have "a + u * b \<le> b + u * a"
```
```   690         by (auto simp add: field_simps)
```
```   691     } note ** = this
```
```   692     then show ?R
```
```   693       unfolding u assms
```
```   694       using u
```
```   695       by (auto simp add: field_simps not_le intro: * **)
```
```   696   }
```
```   697   {
```
```   698     assume ?R
```
```   699     then show ?L
```
```   700     proof (cases "x\$1 = b\$1")
```
```   701       case True
```
```   702       then show ?L
```
```   703         apply (rule_tac x="(x\$1 - a\$1) / (b\$1 - a\$1)" in exI)
```
```   704         unfolding assms True
```
```   705         using \<open>?R\<close>
```
```   706         apply (auto simp add: field_simps)
```
```   707         done
```
```   708     next
```
```   709       case False
```
```   710       then show ?L
```
```   711         apply (rule_tac x="1 - (x\$1 - b\$1) / (a\$1 - b\$1)" in exI)
```
```   712         unfolding assms
```
```   713         using \<open>?R\<close>
```
```   714         apply (auto simp add: field_simps)
```
```   715         done
```
```   716     qed
```
```   717   }
```
```   718 qed
```
```   719
```
```   720
```
```   721 subsection \<open>Useful Fashoda corollary pointed out to me by Tom Hales\<close>
```
```   722
```
```   723 lemma fashoda_interlace:
```
```   724   fixes a :: "real^2"
```
```   725   assumes "path f"
```
```   726     and "path g"
```
```   727     and "path_image f \<subseteq> cbox a b"
```
```   728     and "path_image g \<subseteq> cbox a b"
```
```   729     and "(pathstart f)\$2 = a\$2"
```
```   730     and "(pathfinish f)\$2 = a\$2"
```
```   731     and "(pathstart g)\$2 = a\$2"
```
```   732     and "(pathfinish g)\$2 = a\$2"
```
```   733     and "(pathstart f)\$1 < (pathstart g)\$1"
```
```   734     and "(pathstart g)\$1 < (pathfinish f)\$1"
```
```   735     and "(pathfinish f)\$1 < (pathfinish g)\$1"
```
```   736   obtains z where "z \<in> path_image f" and "z \<in> path_image g"
```
```   737 proof -
```
```   738   have "cbox a b \<noteq> {}"
```
```   739     using path_image_nonempty[of f] using assms(3) by auto
```
```   740   note ab=this[unfolded interval_eq_empty_cart not_ex forall_2 not_less]
```
```   741   have "pathstart f \<in> cbox a b"
```
```   742     and "pathfinish f \<in> cbox a b"
```
```   743     and "pathstart g \<in> cbox a b"
```
```   744     and "pathfinish g \<in> cbox a b"
```
```   745     using pathstart_in_path_image pathfinish_in_path_image
```
```   746     using assms(3-4)
```
```   747     by auto
```
```   748   note startfin = this[unfolded mem_interval_cart forall_2]
```
```   749   let ?P1 = "linepath (vector[a\$1 - 2, a\$2 - 2]) (vector[(pathstart f)\$1,a\$2 - 2]) +++
```
```   750      linepath(vector[(pathstart f)\$1,a\$2 - 2])(pathstart f) +++ f +++
```
```   751      linepath(pathfinish f)(vector[(pathfinish f)\$1,a\$2 - 2]) +++
```
```   752      linepath(vector[(pathfinish f)\$1,a\$2 - 2])(vector[b\$1 + 2,a\$2 - 2])"
```
```   753   let ?P2 = "linepath(vector[(pathstart g)\$1, (pathstart g)\$2 - 3])(pathstart g) +++ g +++
```
```   754      linepath(pathfinish g)(vector[(pathfinish g)\$1,a\$2 - 1]) +++
```
```   755      linepath(vector[(pathfinish g)\$1,a\$2 - 1])(vector[b\$1 + 1,a\$2 - 1]) +++
```
```   756      linepath(vector[b\$1 + 1,a\$2 - 1])(vector[b\$1 + 1,b\$2 + 3])"
```
```   757   let ?a = "vector[a\$1 - 2, a\$2 - 3]"
```
```   758   let ?b = "vector[b\$1 + 2, b\$2 + 3]"
```
```   759   have P1P2: "path_image ?P1 = path_image (linepath (vector[a\$1 - 2, a\$2 - 2]) (vector[(pathstart f)\$1,a\$2 - 2])) \<union>
```
```   760       path_image (linepath(vector[(pathstart f)\$1,a\$2 - 2])(pathstart f)) \<union> path_image f \<union>
```
```   761       path_image (linepath(pathfinish f)(vector[(pathfinish f)\$1,a\$2 - 2])) \<union>
```
```   762       path_image (linepath(vector[(pathfinish f)\$1,a\$2 - 2])(vector[b\$1 + 2,a\$2 - 2]))"
```
```   763     "path_image ?P2 = path_image(linepath(vector[(pathstart g)\$1, (pathstart g)\$2 - 3])(pathstart g)) \<union> path_image g \<union>
```
```   764       path_image(linepath(pathfinish g)(vector[(pathfinish g)\$1,a\$2 - 1])) \<union>
```
```   765       path_image(linepath(vector[(pathfinish g)\$1,a\$2 - 1])(vector[b\$1 + 1,a\$2 - 1])) \<union>
```
```   766       path_image(linepath(vector[b\$1 + 1,a\$2 - 1])(vector[b\$1 + 1,b\$2 + 3]))" using assms(1-2)
```
```   767       by(auto simp add: path_image_join path_linepath)
```
```   768   have abab: "cbox a b \<subseteq> cbox ?a ?b"
```
```   769     unfolding interval_cbox_cart[symmetric]
```
```   770     by (auto simp add:less_eq_vec_def forall_2 vector_2)
```
```   771   obtain z where
```
```   772     "z \<in> path_image
```
```   773           (linepath (vector [a \$ 1 - 2, a \$ 2 - 2]) (vector [pathstart f \$ 1, a \$ 2 - 2]) +++
```
```   774            linepath (vector [pathstart f \$ 1, a \$ 2 - 2]) (pathstart f) +++
```
```   775            f +++
```
```   776            linepath (pathfinish f) (vector [pathfinish f \$ 1, a \$ 2 - 2]) +++
```
```   777            linepath (vector [pathfinish f \$ 1, a \$ 2 - 2]) (vector [b \$ 1 + 2, a \$ 2 - 2]))"
```
```   778     "z \<in> path_image
```
```   779           (linepath (vector [pathstart g \$ 1, pathstart g \$ 2 - 3]) (pathstart g) +++
```
```   780            g +++
```
```   781            linepath (pathfinish g) (vector [pathfinish g \$ 1, a \$ 2 - 1]) +++
```
```   782            linepath (vector [pathfinish g \$ 1, a \$ 2 - 1]) (vector [b \$ 1 + 1, a \$ 2 - 1]) +++
```
```   783            linepath (vector [b \$ 1 + 1, a \$ 2 - 1]) (vector [b \$ 1 + 1, b \$ 2 + 3]))"
```
```   784     apply (rule fashoda[of ?P1 ?P2 ?a ?b])
```
```   785     unfolding pathstart_join pathfinish_join pathstart_linepath pathfinish_linepath vector_2
```
```   786   proof -
```
```   787     show "path ?P1" and "path ?P2"
```
```   788       using assms by auto
```
```   789     have "path_image ?P1 \<subseteq> cbox ?a ?b"
```
```   790       unfolding P1P2 path_image_linepath
```
```   791       apply (rule Un_least)+
```
```   792       defer 3
```
```   793       apply (rule_tac[1-4] convex_box(1)[unfolded convex_contains_segment,rule_format])
```
```   794       unfolding mem_interval_cart forall_2 vector_2
```
```   795       using ab startfin abab assms(3)
```
```   796       using assms(9-)
```
```   797       unfolding assms
```
```   798       apply (auto simp add: field_simps box_def)
```
```   799       done
```
```   800     then show "path_image ?P1 \<subseteq> cbox ?a ?b" .
```
```   801     have "path_image ?P2 \<subseteq> cbox ?a ?b"
```
```   802       unfolding P1P2 path_image_linepath
```
```   803       apply (rule Un_least)+
```
```   804       defer 2
```
```   805       apply (rule_tac[1-4] convex_box(1)[unfolded convex_contains_segment,rule_format])
```
```   806       unfolding mem_interval_cart forall_2 vector_2
```
```   807       using ab startfin abab assms(4)
```
```   808       using assms(9-)
```
```   809       unfolding assms
```
```   810       apply (auto simp add: field_simps box_def)
```
```   811       done
```
```   812     then show "path_image ?P2 \<subseteq> cbox ?a ?b" .
```
```   813     show "a \$ 1 - 2 = a \$ 1 - 2"
```
```   814       and "b \$ 1 + 2 = b \$ 1 + 2"
```
```   815       and "pathstart g \$ 2 - 3 = a \$ 2 - 3"
```
```   816       and "b \$ 2 + 3 = b \$ 2 + 3"
```
```   817       by (auto simp add: assms)
```
```   818   qed
```
```   819   note z=this[unfolded P1P2 path_image_linepath]
```
```   820   show thesis
```
```   821     apply (rule that[of z])
```
```   822   proof -
```
```   823     have "(z \<in> closed_segment (vector [a \$ 1 - 2, a \$ 2 - 2]) (vector [pathstart f \$ 1, a \$ 2 - 2]) \<or>
```
```   824       z \<in> closed_segment (vector [pathstart f \$ 1, a \$ 2 - 2]) (pathstart f)) \<or>
```
```   825       z \<in> closed_segment (pathfinish f) (vector [pathfinish f \$ 1, a \$ 2 - 2]) \<or>
```
```   826       z \<in> closed_segment (vector [pathfinish f \$ 1, a \$ 2 - 2]) (vector [b \$ 1 + 2, a \$ 2 - 2]) \<Longrightarrow>
```
```   827     (((z \<in> closed_segment (vector [pathstart g \$ 1, pathstart g \$ 2 - 3]) (pathstart g)) \<or>
```
```   828       z \<in> closed_segment (pathfinish g) (vector [pathfinish g \$ 1, a \$ 2 - 1])) \<or>
```
```   829       z \<in> closed_segment (vector [pathfinish g \$ 1, a \$ 2 - 1]) (vector [b \$ 1 + 1, a \$ 2 - 1])) \<or>
```
```   830       z \<in> closed_segment (vector [b \$ 1 + 1, a \$ 2 - 1]) (vector [b \$ 1 + 1, b \$ 2 + 3]) \<Longrightarrow> False"
```
```   831     proof (simp only: segment_vertical segment_horizontal vector_2, goal_cases)
```
```   832       case prems: 1
```
```   833       have "pathfinish f \<in> cbox a b"
```
```   834         using assms(3) pathfinish_in_path_image[of f] by auto
```
```   835       then have "1 + b \$ 1 \<le> pathfinish f \$ 1 \<Longrightarrow> False"
```
```   836         unfolding mem_interval_cart forall_2 by auto
```
```   837       then have "z\$1 \<noteq> pathfinish f\$1"
```
```   838         using prems(2)
```
```   839         using assms ab
```
```   840         by (auto simp add: field_simps)
```
```   841       moreover have "pathstart f \<in> cbox a b"
```
```   842         using assms(3) pathstart_in_path_image[of f]
```
```   843         by auto
```
```   844       then have "1 + b \$ 1 \<le> pathstart f \$ 1 \<Longrightarrow> False"
```
```   845         unfolding mem_interval_cart forall_2
```
```   846         by auto
```
```   847       then have "z\$1 \<noteq> pathstart f\$1"
```
```   848         using prems(2) using assms ab
```
```   849         by (auto simp add: field_simps)
```
```   850       ultimately have *: "z\$2 = a\$2 - 2"
```
```   851         using prems(1)
```
```   852         by auto
```
```   853       have "z\$1 \<noteq> pathfinish g\$1"
```
```   854         using prems(2)
```
```   855         using assms ab
```
```   856         by (auto simp add: field_simps *)
```
```   857       moreover have "pathstart g \<in> cbox a b"
```
```   858         using assms(4) pathstart_in_path_image[of g]
```
```   859         by auto
```
```   860       note this[unfolded mem_interval_cart forall_2]
```
```   861       then have "z\$1 \<noteq> pathstart g\$1"
```
```   862         using prems(1)
```
```   863         using assms ab
```
```   864         by (auto simp add: field_simps *)
```
```   865       ultimately have "a \$ 2 - 1 \<le> z \$ 2 \<and> z \$ 2 \<le> b \$ 2 + 3 \<or> b \$ 2 + 3 \<le> z \$ 2 \<and> z \$ 2 \<le> a \$ 2 - 1"
```
```   866         using prems(2)
```
```   867         unfolding * assms
```
```   868         by (auto simp add: field_simps)
```
```   869       then show False
```
```   870         unfolding * using ab by auto
```
```   871     qed
```
```   872     then have "z \<in> path_image f \<or> z \<in> path_image g"
```
```   873       using z unfolding Un_iff by blast
```
```   874     then have z': "z \<in> cbox a b"
```
```   875       using assms(3-4)
```
```   876       by auto
```
```   877     have "a \$ 2 = z \$ 2 \<Longrightarrow> (z \$ 1 = pathstart f \$ 1 \<or> z \$ 1 = pathfinish f \$ 1) \<Longrightarrow>
```
```   878       z = pathstart f \<or> z = pathfinish f"
```
```   879       unfolding vec_eq_iff forall_2 assms
```
```   880       by auto
```
```   881     with z' show "z \<in> path_image f"
```
```   882       using z(1)
```
```   883       unfolding Un_iff mem_interval_cart forall_2
```
```   884       apply -
```
```   885       apply (simp only: segment_vertical segment_horizontal vector_2)
```
```   886       unfolding assms
```
```   887       apply auto
```
```   888       done
```
```   889     have "a \$ 2 = z \$ 2 \<Longrightarrow> (z \$ 1 = pathstart g \$ 1 \<or> z \$ 1 = pathfinish g \$ 1) \<Longrightarrow>
```
```   890       z = pathstart g \<or> z = pathfinish g"
```
```   891       unfolding vec_eq_iff forall_2 assms
```
```   892       by auto
```
```   893     with z' show "z \<in> path_image g"
```
```   894       using z(2)
```
```   895       unfolding Un_iff mem_interval_cart forall_2
```
```   896       apply (simp only: segment_vertical segment_horizontal vector_2)
```
```   897       unfolding assms
```
```   898       apply auto
```
```   899       done
```
```   900   qed
```
```   901 qed
```
```   902
```
```   903 (** The Following still needs to be translated. Maybe I will do that later.
```
```   904
```
```   905 (* ------------------------------------------------------------------------- *)
```
```   906 (* Complement in dimension N >= 2 of set homeomorphic to any interval in     *)
```
```   907 (* any dimension is (path-)connected. This naively generalizes the argument  *)
```
```   908 (* in Ryuji Maehara's paper "The Jordan curve theorem via the Brouwer        *)
```
```   909 (* fixed point theorem", American Mathematical Monthly 1984.                 *)
```
```   910 (* ------------------------------------------------------------------------- *)
```
```   911
```
```   912 let RETRACTION_INJECTIVE_IMAGE_INTERVAL = prove
```
```   913  (`!p:real^M->real^N a b.
```
```   914         ~(interval[a,b] = {}) /\
```
```   915         p continuous_on interval[a,b] /\
```
```   916         (!x y. x IN interval[a,b] /\ y IN interval[a,b] /\ p x = p y ==> x = y)
```
```   917         ==> ?f. f continuous_on (:real^N) /\
```
```   918                 IMAGE f (:real^N) SUBSET (IMAGE p (interval[a,b])) /\
```
```   919                 (!x. x IN (IMAGE p (interval[a,b])) ==> f x = x)`,
```
```   920   REPEAT STRIP_TAC THEN
```
```   921   FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [INJECTIVE_ON_LEFT_INVERSE]) THEN
```
```   922   DISCH_THEN(X_CHOOSE_TAC `q:real^N->real^M`) THEN
```
```   923   SUBGOAL_THEN `(q:real^N->real^M) continuous_on
```
```   924                 (IMAGE p (interval[a:real^M,b]))`
```
```   925   ASSUME_TAC THENL
```
```   926    [MATCH_MP_TAC CONTINUOUS_ON_INVERSE THEN ASM_REWRITE_TAC[COMPACT_INTERVAL];
```
```   927     ALL_TAC] THEN
```
```   928   MP_TAC(ISPECL [`q:real^N->real^M`;
```
```   929                  `IMAGE (p:real^M->real^N)
```
```   930                  (interval[a,b])`;
```
```   931                  `a:real^M`; `b:real^M`]
```
```   932         TIETZE_CLOSED_INTERVAL) THEN
```
```   933   ASM_SIMP_TAC[COMPACT_INTERVAL; COMPACT_CONTINUOUS_IMAGE;
```
```   934                COMPACT_IMP_CLOSED] THEN
```
```   935   ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
```
```   936   DISCH_THEN(X_CHOOSE_THEN `r:real^N->real^M` STRIP_ASSUME_TAC) THEN
```
```   937   EXISTS_TAC `(p:real^M->real^N) o (r:real^N->real^M)` THEN
```
```   938   REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; o_THM; IN_UNIV] THEN
```
```   939   CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
```
```   940   MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN ASM_REWRITE_TAC[] THEN
```
```   941   FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP(REWRITE_RULE[IMP_CONJ]
```
```   942         CONTINUOUS_ON_SUBSET)) THEN ASM SET_TAC[]);;
```
```   943
```
```   944 let UNBOUNDED_PATH_COMPONENTS_COMPLEMENT_HOMEOMORPHIC_INTERVAL = prove
```
```   945  (`!s:real^N->bool a b:real^M.
```
```   946         s homeomorphic (interval[a,b])
```
```   947         ==> !x. ~(x IN s) ==> ~bounded(path_component((:real^N) DIFF s) x)`,
```
```   948   REPEAT GEN_TAC THEN REWRITE_TAC[homeomorphic; homeomorphism] THEN
```
```   949   REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
```
```   950   MAP_EVERY X_GEN_TAC [`p':real^N->real^M`; `p:real^M->real^N`] THEN
```
```   951   DISCH_TAC THEN
```
```   952   SUBGOAL_THEN
```
```   953    `!x y. x IN interval[a,b] /\ y IN interval[a,b] /\
```
```   954           (p:real^M->real^N) x = p y ==> x = y`
```
```   955   ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
```
```   956   FIRST_X_ASSUM(MP_TAC o funpow 4 CONJUNCT2) THEN
```
```   957   DISCH_THEN(CONJUNCTS_THEN2 (SUBST1_TAC o SYM) ASSUME_TAC) THEN
```
```   958   ASM_CASES_TAC `interval[a:real^M,b] = {}` THEN
```
```   959   ASM_REWRITE_TAC[IMAGE_CLAUSES; DIFF_EMPTY; PATH_COMPONENT_UNIV;
```
```   960                   NOT_BOUNDED_UNIV] THEN
```
```   961   ABBREV_TAC `s = (:real^N) DIFF (IMAGE p (interval[a:real^M,b]))` THEN
```
```   962   X_GEN_TAC `c:real^N` THEN REPEAT STRIP_TAC THEN
```
```   963   SUBGOAL_THEN `(c:real^N) IN s` ASSUME_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
```
```   964   SUBGOAL_THEN `bounded((path_component s c) UNION
```
```   965                         (IMAGE (p:real^M->real^N) (interval[a,b])))`
```
```   966   MP_TAC THENL
```
```   967    [ASM_SIMP_TAC[BOUNDED_UNION; COMPACT_IMP_BOUNDED; COMPACT_IMP_BOUNDED;
```
```   968                  COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL];
```
```   969     ALL_TAC] THEN
```
```   970   DISCH_THEN(MP_TAC o SPEC `c:real^N` o MATCH_MP BOUNDED_SUBSET_BALL) THEN
```
```   971   REWRITE_TAC[UNION_SUBSET] THEN
```
```   972   DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC) THEN
```
```   973   MP_TAC(ISPECL [`p:real^M->real^N`; `a:real^M`; `b:real^M`]
```
```   974     RETRACTION_INJECTIVE_IMAGE_INTERVAL) THEN
```
```   975   ASM_REWRITE_TAC[SUBSET; IN_UNIV] THEN
```
```   976   DISCH_THEN(X_CHOOSE_THEN `r:real^N->real^N` MP_TAC) THEN
```
```   977   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC
```
```   978    (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN
```
```   979   REWRITE_TAC[FORALL_IN_IMAGE; IN_UNIV] THEN DISCH_TAC THEN
```
```   980   ABBREV_TAC `q = \z:real^N. if z IN path_component s c then r(z) else z` THEN
```
```   981   SUBGOAL_THEN
```
```   982     `(q:real^N->real^N) continuous_on
```
```   983      (closure(path_component s c) UNION ((:real^N) DIFF (path_component s c)))`
```
```   984   MP_TAC THENL
```
```   985    [EXPAND_TAC "q" THEN MATCH_MP_TAC CONTINUOUS_ON_CASES THEN
```
```   986     REWRITE_TAC[CLOSED_CLOSURE; CONTINUOUS_ON_ID; GSYM OPEN_CLOSED] THEN
```
```   987     REPEAT CONJ_TAC THENL
```
```   988      [MATCH_MP_TAC OPEN_PATH_COMPONENT THEN EXPAND_TAC "s" THEN
```
```   989       ASM_SIMP_TAC[GSYM CLOSED_OPEN; COMPACT_IMP_CLOSED;
```
```   990                    COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL];
```
```   991       ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; SUBSET_UNIV];
```
```   992       ALL_TAC] THEN
```
```   993     X_GEN_TAC `z:real^N` THEN
```
```   994     REWRITE_TAC[SET_RULE `~(z IN (s DIFF t) /\ z IN t)`] THEN
```
```   995     STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
```
```   996     MP_TAC(ISPECL
```
```   997      [`path_component s (z:real^N)`; `path_component s (c:real^N)`]
```
```   998      OPEN_INTER_CLOSURE_EQ_EMPTY) THEN
```
```   999     ASM_REWRITE_TAC[GSYM DISJOINT; PATH_COMPONENT_DISJOINT] THEN ANTS_TAC THENL
```
```  1000      [MATCH_MP_TAC OPEN_PATH_COMPONENT THEN EXPAND_TAC "s" THEN
```
```  1001       ASM_SIMP_TAC[GSYM CLOSED_OPEN; COMPACT_IMP_CLOSED;
```
```  1002                    COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL];
```
```  1003       REWRITE_TAC[DISJOINT; EXTENSION; IN_INTER; NOT_IN_EMPTY] THEN
```
```  1004       DISCH_THEN(MP_TAC o SPEC `z:real^N`) THEN ASM_REWRITE_TAC[] THEN
```
```  1005       GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [IN] THEN
```
```  1006       REWRITE_TAC[PATH_COMPONENT_REFL_EQ] THEN ASM SET_TAC[]];
```
```  1007     ALL_TAC] THEN
```
```  1008   SUBGOAL_THEN
```
```  1009    `closure(path_component s c) UNION ((:real^N) DIFF (path_component s c)) =
```
```  1010     (:real^N)`
```
```  1011   SUBST1_TAC THENL
```
```  1012    [MATCH_MP_TAC(SET_RULE `s SUBSET t ==> t UNION (UNIV DIFF s) = UNIV`) THEN
```
```  1013     REWRITE_TAC[CLOSURE_SUBSET];
```
```  1014     DISCH_TAC] THEN
```
```  1015   MP_TAC(ISPECL
```
```  1016    [`(\x. &2 % c - x) o
```
```  1017      (\x. c + B / norm(x - c) % (x - c)) o (q:real^N->real^N)`;
```
```  1018     `cball(c:real^N,B)`]
```
```  1019     BROUWER) THEN
```
```  1020   REWRITE_TAC[NOT_IMP; GSYM CONJ_ASSOC; COMPACT_CBALL; CONVEX_CBALL] THEN
```
```  1021   ASM_SIMP_TAC[CBALL_EQ_EMPTY; REAL_LT_IMP_LE; REAL_NOT_LT] THEN
```
```  1022   SUBGOAL_THEN `!x. ~((q:real^N->real^N) x = c)` ASSUME_TAC THENL
```
```  1023    [X_GEN_TAC `x:real^N` THEN EXPAND_TAC "q" THEN
```
```  1024     REWRITE_TAC[NORM_EQ_0; VECTOR_SUB_EQ] THEN COND_CASES_TAC THEN
```
```  1025     ASM SET_TAC[PATH_COMPONENT_REFL_EQ];
```
```  1026     ALL_TAC] THEN
```
```  1027   REPEAT CONJ_TAC THENL
```
```  1028    [MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
```
```  1029     SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST] THEN
```
```  1030     MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN CONJ_TAC THENL
```
```  1031      [ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; SUBSET_UNIV]; ALL_TAC] THEN
```
```  1032     MATCH_MP_TAC CONTINUOUS_ON_ADD THEN REWRITE_TAC[CONTINUOUS_ON_CONST] THEN
```
```  1033     MATCH_MP_TAC CONTINUOUS_ON_MUL THEN
```
```  1034     SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST] THEN
```
```  1035     REWRITE_TAC[o_DEF; real_div; LIFT_CMUL] THEN
```
```  1036     MATCH_MP_TAC CONTINUOUS_ON_CMUL THEN
```
```  1037     MATCH_MP_TAC(REWRITE_RULE[o_DEF] CONTINUOUS_ON_INV) THEN
```
```  1038     ASM_REWRITE_TAC[FORALL_IN_IMAGE; NORM_EQ_0; VECTOR_SUB_EQ] THEN
```
```  1039     SUBGOAL_THEN
```
```  1040      `(\x:real^N. lift(norm(x - c))) = (lift o norm) o (\x. x - c)`
```
```  1041     SUBST1_TAC THENL [REWRITE_TAC[o_DEF]; ALL_TAC] THEN
```
```  1042     MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
```
```  1043     ASM_SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST;
```
```  1044                  CONTINUOUS_ON_LIFT_NORM];
```
```  1045     REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_CBALL; o_THM; dist] THEN
```
```  1046     X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
```
```  1047     REWRITE_TAC[VECTOR_ARITH `c - (&2 % c - (c + x)) = x`] THEN
```
```  1048     REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM] THEN
```
```  1049     ASM_SIMP_TAC[REAL_DIV_RMUL; NORM_EQ_0; VECTOR_SUB_EQ] THEN
```
```  1050     ASM_REAL_ARITH_TAC;
```
```  1051     REWRITE_TAC[NOT_EXISTS_THM; TAUT `~(c /\ b) <=> c ==> ~b`] THEN
```
```  1052     REWRITE_TAC[IN_CBALL; o_THM; dist] THEN
```
```  1053     X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
```
```  1054     REWRITE_TAC[VECTOR_ARITH `&2 % c - (c + x') = x <=> --x' = x - c`] THEN
```
```  1055     ASM_CASES_TAC `(x:real^N) IN path_component s c` THENL
```
```  1056      [MATCH_MP_TAC(NORM_ARITH `norm(y) < B /\ norm(x) = B ==> ~(--x = y)`) THEN
```
```  1057       REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM] THEN
```
```  1058       ASM_SIMP_TAC[REAL_DIV_RMUL; NORM_EQ_0; VECTOR_SUB_EQ] THEN
```
```  1059       ASM_SIMP_TAC[REAL_ARITH `&0 < B ==> abs B = B`] THEN
```
```  1060       UNDISCH_TAC `path_component s c SUBSET ball(c:real^N,B)` THEN
```
```  1061       REWRITE_TAC[SUBSET; IN_BALL] THEN ASM_MESON_TAC[dist; NORM_SUB];
```
```  1062       EXPAND_TAC "q" THEN REWRITE_TAC[] THEN ASM_REWRITE_TAC[] THEN
```
```  1063       REWRITE_TAC[VECTOR_ARITH `--(c % x) = x <=> (&1 + c) % x = vec 0`] THEN
```
```  1064       ASM_REWRITE_TAC[DE_MORGAN_THM; VECTOR_SUB_EQ; VECTOR_MUL_EQ_0] THEN
```
```  1065       SUBGOAL_THEN `~(x:real^N = c)` ASSUME_TAC THENL
```
```  1066        [ASM_MESON_TAC[PATH_COMPONENT_REFL; IN]; ALL_TAC] THEN
```
```  1067       ASM_REWRITE_TAC[] THEN
```
```  1068       MATCH_MP_TAC(REAL_ARITH `&0 < x ==> ~(&1 + x = &0)`) THEN
```
```  1069       ASM_SIMP_TAC[REAL_LT_DIV; NORM_POS_LT; VECTOR_SUB_EQ]]]);;
```
```  1070
```
```  1071 let PATH_CONNECTED_COMPLEMENT_HOMEOMORPHIC_INTERVAL = prove
```
```  1072  (`!s:real^N->bool a b:real^M.
```
```  1073         2 <= dimindex(:N) /\ s homeomorphic interval[a,b]
```
```  1074         ==> path_connected((:real^N) DIFF s)`,
```
```  1075   REPEAT STRIP_TAC THEN REWRITE_TAC[PATH_CONNECTED_IFF_PATH_COMPONENT] THEN
```
```  1076   FIRST_ASSUM(MP_TAC o MATCH_MP
```
```  1077     UNBOUNDED_PATH_COMPONENTS_COMPLEMENT_HOMEOMORPHIC_INTERVAL) THEN
```
```  1078   ASM_REWRITE_TAC[SET_RULE `~(x IN s) <=> x IN (UNIV DIFF s)`] THEN
```
```  1079   ABBREV_TAC `t = (:real^N) DIFF s` THEN
```
```  1080   DISCH_TAC THEN MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`] THEN
```
```  1081   STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP HOMEOMORPHIC_COMPACTNESS) THEN
```
```  1082   REWRITE_TAC[COMPACT_INTERVAL] THEN
```
```  1083   DISCH_THEN(MP_TAC o MATCH_MP COMPACT_IMP_BOUNDED) THEN
```
```  1084   REWRITE_TAC[BOUNDED_POS; LEFT_IMP_EXISTS_THM] THEN
```
```  1085   X_GEN_TAC `B:real` THEN STRIP_TAC THEN
```
```  1086   SUBGOAL_THEN `(?u:real^N. u IN path_component t x /\ B < norm(u)) /\
```
```  1087                 (?v:real^N. v IN path_component t y /\ B < norm(v))`
```
```  1088   STRIP_ASSUME_TAC THENL
```
```  1089    [ASM_MESON_TAC[BOUNDED_POS; REAL_NOT_LE]; ALL_TAC] THEN
```
```  1090   MATCH_MP_TAC PATH_COMPONENT_TRANS THEN EXISTS_TAC `u:real^N` THEN
```
```  1091   CONJ_TAC THENL [ASM_MESON_TAC[IN]; ALL_TAC] THEN
```
```  1092   MATCH_MP_TAC PATH_COMPONENT_SYM THEN
```
```  1093   MATCH_MP_TAC PATH_COMPONENT_TRANS THEN EXISTS_TAC `v:real^N` THEN
```
```  1094   CONJ_TAC THENL [ASM_MESON_TAC[IN]; ALL_TAC] THEN
```
```  1095   MATCH_MP_TAC PATH_COMPONENT_OF_SUBSET THEN
```
```  1096   EXISTS_TAC `(:real^N) DIFF cball(vec 0,B)` THEN CONJ_TAC THENL
```
```  1097    [EXPAND_TAC "t" THEN MATCH_MP_TAC(SET_RULE
```
```  1098      `s SUBSET t ==> (u DIFF t) SUBSET (u DIFF s)`) THEN
```
```  1099     ASM_REWRITE_TAC[SUBSET; IN_CBALL_0];
```
```  1100     MP_TAC(ISPEC `cball(vec 0:real^N,B)`
```
```  1101        PATH_CONNECTED_COMPLEMENT_BOUNDED_CONVEX) THEN
```
```  1102     ASM_REWRITE_TAC[BOUNDED_CBALL; CONVEX_CBALL] THEN
```
```  1103     REWRITE_TAC[PATH_CONNECTED_IFF_PATH_COMPONENT] THEN
```
```  1104     DISCH_THEN MATCH_MP_TAC THEN
```
```  1105     ASM_REWRITE_TAC[IN_DIFF; IN_UNIV; IN_CBALL_0; REAL_NOT_LE]]);;
```
```  1106
```
```  1107 (* ------------------------------------------------------------------------- *)
```
```  1108 (* In particular, apply all these to the special case of an arc.             *)
```
```  1109 (* ------------------------------------------------------------------------- *)
```
```  1110
```
```  1111 let RETRACTION_ARC = prove
```
```  1112  (`!p. arc p
```
```  1113        ==> ?f. f continuous_on (:real^N) /\
```
```  1114                IMAGE f (:real^N) SUBSET path_image p /\
```
```  1115                (!x. x IN path_image p ==> f x = x)`,
```
```  1116   REWRITE_TAC[arc; path; path_image] THEN REPEAT STRIP_TAC THEN
```
```  1117   MATCH_MP_TAC RETRACTION_INJECTIVE_IMAGE_INTERVAL THEN
```
```  1118   ASM_REWRITE_TAC[INTERVAL_EQ_EMPTY_CART_1; DROP_VEC; REAL_NOT_LT; REAL_POS]);;
```
```  1119
```
```  1120 let PATH_CONNECTED_ARC_COMPLEMENT = prove
```
```  1121  (`!p. 2 <= dimindex(:N) /\ arc p
```
```  1122        ==> path_connected((:real^N) DIFF path_image p)`,
```
```  1123   REWRITE_TAC[arc; path] THEN REPEAT STRIP_TAC THEN SIMP_TAC[path_image] THEN
```
```  1124   MP_TAC(ISPECL [`path_image p:real^N->bool`; `vec 0:real^1`; `vec 1:real^1`]
```
```  1125     PATH_CONNECTED_COMPLEMENT_HOMEOMORPHIC_INTERVAL) THEN
```
```  1126   ASM_REWRITE_TAC[path_image] THEN DISCH_THEN MATCH_MP_TAC THEN
```
```  1127   ONCE_REWRITE_TAC[HOMEOMORPHIC_SYM] THEN
```
```  1128   MATCH_MP_TAC HOMEOMORPHIC_COMPACT THEN
```
```  1129   EXISTS_TAC `p:real^1->real^N` THEN ASM_REWRITE_TAC[COMPACT_INTERVAL]);;
```
```  1130
```
```  1131 let CONNECTED_ARC_COMPLEMENT = prove
```
```  1132  (`!p. 2 <= dimindex(:N) /\ arc p
```
```  1133        ==> connected((:real^N) DIFF path_image p)`,
```
```  1134   SIMP_TAC[PATH_CONNECTED_ARC_COMPLEMENT; PATH_CONNECTED_IMP_CONNECTED]);; *)
```
```  1135
```
```  1136 end
```