src/HOL/Analysis/Fashoda_Theorem.thy
 author wenzelm Mon Mar 25 17:21:26 2019 +0100 (2 months ago) changeset 69981 3dced198b9ec parent 69722 b5163b2132c5 child 70136 f03a01a18c6e permissions -rw-r--r--
more strict AFP properties;
```     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%important 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: sum.distrib[symmetric] scaleR_add_left[symmetric] interval_bij_def fun_eq_iff
```
```    21     field_simps inner_simps add_divide_distrib[symmetric] intro!: sum.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_sum 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_sum_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 proposition 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 infnorm_mul[unfolded scalar_mult_eq_scaleR]
```
```   113     by (simp add: real_abs_infnorm infnorm_eq_0)
```
```   114   let ?F = "\<lambda>w::real^2. (f \<circ> (\<lambda>x. x\$1)) w - (g \<circ> (\<lambda>x. x\$2)) w"
```
```   115   have *: "\<And>i. (\<lambda>x::real^2. x \$ i) ` cbox (- 1) 1 = {-1..1}"
```
```   116   proof
```
```   117     show "(\<lambda>x::real^2. x \$ i) ` cbox (- 1) 1 \<subseteq> {-1..1}" for i
```
```   118       by (auto simp: mem_box_cart)
```
```   119     show "{-1..1} \<subseteq> (\<lambda>x::real^2. x \$ i) ` cbox (- 1) 1" for i
```
```   120       by (clarsimp simp: image_iff mem_box_cart Bex_def) (metis (no_types, hide_lams) vec_component)
```
```   121   qed
```
```   122   {
```
```   123     fix x
```
```   124     assume "x \<in> (\<lambda>w. (f \<circ> (\<lambda>x. x \$ 1)) w - (g \<circ> (\<lambda>x. x \$ 2)) w) ` (cbox (- 1) (1::real^2))"
```
```   125     then obtain w :: "real^2" where w:
```
```   126         "w \<in> cbox (- 1) 1"
```
```   127         "x = (f \<circ> (\<lambda>x. x \$ 1)) w - (g \<circ> (\<lambda>x. x \$ 2)) w"
```
```   128       unfolding image_iff ..
```
```   129     then have "x \<noteq> 0"
```
```   130       using as[of "w\$1" "w\$2"]
```
```   131       unfolding mem_box_cart atLeastAtMost_iff
```
```   132       by auto
```
```   133   } note x0 = this
```
```   134   have 1: "box (- 1) (1::real^2) \<noteq> {}"
```
```   135     unfolding interval_eq_empty_cart by auto
```
```   136   have "negatex (x + y) \$ i = (negatex x + negatex y) \$ i \<and> negatex (c *\<^sub>R x) \$ i = (c *\<^sub>R negatex x) \$ i"
```
```   137     for i x y c
```
```   138     using exhaust_2 [of i] by (auto simp: negatex_def)
```
```   139   then have "bounded_linear negatex"
```
```   140     by (simp add: bounded_linearI' vec_eq_iff)
```
```   141   then have 2: "continuous_on (cbox (- 1) 1) (negatex \<circ> sqprojection \<circ> ?F)"
```
```   142     apply (intro continuous_intros continuous_on_component)
```
```   143     unfolding * sqprojection_def
```
```   144     apply (intro assms continuous_intros)+
```
```   145      apply (simp_all add: infnorm_eq_0 x0 linear_continuous_on)
```
```   146     done
```
```   147   have 3: "(negatex \<circ> sqprojection \<circ> ?F) ` cbox (-1) 1 \<subseteq> cbox (-1) 1"
```
```   148     unfolding subset_eq
```
```   149   proof (rule, goal_cases)
```
```   150     case (1 x)
```
```   151     then obtain y :: "real^2" where y:
```
```   152         "y \<in> cbox (- 1) 1"
```
```   153         "x = (negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x \$ 1)) w - (g \<circ> (\<lambda>x. x \$ 2)) w)) y"
```
```   154       unfolding image_iff ..
```
```   155     have "?F y \<noteq> 0"
```
```   156       by (rule x0) (use y in auto)
```
```   157     then have *: "infnorm (sqprojection (?F y)) = 1"
```
```   158       unfolding y o_def
```
```   159       by - (rule lem2[rule_format])
```
```   160     have inf1: "infnorm x = 1"
```
```   161       unfolding *[symmetric] y o_def
```
```   162       by (rule lem1[rule_format])
```
```   163     show "x \<in> cbox (-1) 1"
```
```   164       unfolding mem_box_cart interval_cbox_cart infnorm_2
```
```   165     proof
```
```   166       fix i
```
```   167       show "(- 1) \$ i \<le> x \$ i \<and> x \$ i \<le> 1 \$ i"
```
```   168         using exhaust_2 [of i] inf1 by (auto simp: infnorm_2)
```
```   169     qed
```
```   170   qed
```
```   171   obtain x :: "real^2" where x:
```
```   172       "x \<in> cbox (- 1) 1"
```
```   173       "(negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x \$ 1)) w - (g \<circ> (\<lambda>x. x \$ 2)) w)) x = x"
```
```   174     apply (rule brouwer_weak[of "cbox (- 1) (1::real^2)" "negatex \<circ> sqprojection \<circ> ?F"])
```
```   175     apply (rule compact_cbox convex_box)+
```
```   176     unfolding interior_cbox
```
```   177     apply (rule 1 2 3)+
```
```   178     apply blast
```
```   179     done
```
```   180   have "?F x \<noteq> 0"
```
```   181     by (rule x0) (use x in auto)
```
```   182   then have *: "infnorm (sqprojection (?F x)) = 1"
```
```   183     unfolding o_def
```
```   184     by (rule lem2[rule_format])
```
```   185   have nx: "infnorm x = 1"
```
```   186     apply (subst x(2)[symmetric])
```
```   187     unfolding *[symmetric] o_def
```
```   188     apply (rule lem1[rule_format])
```
```   189     done
```
```   190   have iff: "0 < sqprojection x\$i \<longleftrightarrow> 0 < x\$i" "sqprojection x\$i < 0 \<longleftrightarrow> x\$i < 0" if "x \<noteq> 0" for x i
```
```   191   proof -
```
```   192     have "inverse (infnorm x) > 0"
```
```   193       by (simp add: infnorm_pos_lt that)
```
```   194     then show "(0 < sqprojection x \$ i) = (0 < x \$ i)"
```
```   195       and "(sqprojection x \$ i < 0) = (x \$ i < 0)"
```
```   196       unfolding sqprojection_def vector_component_simps vector_scaleR_component real_scaleR_def
```
```   197       unfolding zero_less_mult_iff mult_less_0_iff
```
```   198       by (auto simp add: field_simps)
```
```   199   qed
```
```   200   have x1: "x \$ 1 \<in> {- 1..1::real}" "x \$ 2 \<in> {- 1..1::real}"
```
```   201     using x(1) unfolding mem_box_cart by auto
```
```   202   then have nz: "f (x \$ 1) - g (x \$ 2) \<noteq> 0"
```
```   203     using as by auto
```
```   204   consider "x \$ 1 = -1" | "x \$ 1 = 1" | "x \$ 2 = -1" | "x \$ 2 = 1"
```
```   205     using nx unfolding infnorm_eq_1_2 by auto
```
```   206   then show False
```
```   207   proof cases
```
```   208     case 1
```
```   209     then have *: "f (x \$ 1) \$ 1 = - 1"
```
```   210       using assms(5) by auto
```
```   211     have "sqprojection (f (x\$1) - g (x\$2)) \$ 1 > 0"
```
```   212       using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]]
```
```   213       by (auto simp: negatex_def 1)
```
```   214     moreover
```
```   215     from x1 have "g (x \$ 2) \<in> cbox (-1) 1"
```
```   216       using assms(2) by blast
```
```   217     ultimately show False
```
```   218       unfolding iff[OF nz] vector_component_simps * mem_box_cart
```
```   219       using not_le by auto
```
```   220   next
```
```   221     case 2
```
```   222     then have *: "f (x \$ 1) \$ 1 = 1"
```
```   223       using assms(6) by auto
```
```   224     have "sqprojection (f (x\$1) - g (x\$2)) \$ 1 < 0"
```
```   225       using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]] 2
```
```   226       by (auto simp: negatex_def)
```
```   227     moreover have "g (x \$ 2) \<in> cbox (-1) 1"
```
```   228       using assms(2) x1 by blast
```
```   229     ultimately show False
```
```   230       unfolding iff[OF nz] vector_component_simps * mem_box_cart
```
```   231       using not_le by auto
```
```   232   next
```
```   233     case 3
```
```   234     then have *: "g (x \$ 2) \$ 2 = - 1"
```
```   235       using assms(7) by auto
```
```   236     have "sqprojection (f (x\$1) - g (x\$2)) \$ 2 < 0"
```
```   237       using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]] 3 by (auto simp: negatex_def)
```
```   238     moreover
```
```   239     from x1 have "f (x \$ 1) \<in> cbox (-1) 1"
```
```   240       using assms(1) by blast
```
```   241     ultimately show False
```
```   242       unfolding iff[OF nz] vector_component_simps * mem_box_cart
```
```   243       by (erule_tac x=2 in allE) auto
```
```   244   next
```
```   245     case 4
```
```   246     then have *: "g (x \$ 2) \$ 2 = 1"
```
```   247       using assms(8) by auto
```
```   248     have "sqprojection (f (x\$1) - g (x\$2)) \$ 2 > 0"
```
```   249       using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]] 4 by (auto simp: negatex_def)
```
```   250     moreover
```
```   251     from x1 have "f (x \$ 1) \<in> cbox (-1) 1"
```
```   252       using assms(1) by blast
```
```   253     ultimately show False
```
```   254       unfolding iff[OF nz] vector_component_simps * mem_box_cart
```
```   255       by (erule_tac x=2 in allE) auto
```
```   256   qed
```
```   257 qed
```
```   258
```
```   259 proposition fashoda_unit_path:
```
```   260   fixes f g :: "real \<Rightarrow> real^2"
```
```   261   assumes "path f"
```
```   262     and "path g"
```
```   263     and "path_image f \<subseteq> cbox (-1) 1"
```
```   264     and "path_image g \<subseteq> cbox (-1) 1"
```
```   265     and "(pathstart f)\$1 = -1"
```
```   266     and "(pathfinish f)\$1 = 1"
```
```   267     and "(pathstart g)\$2 = -1"
```
```   268     and "(pathfinish g)\$2 = 1"
```
```   269   obtains z where "z \<in> path_image f" and "z \<in> path_image g"
```
```   270 proof -
```
```   271   note assms=assms[unfolded path_def pathstart_def pathfinish_def path_image_def]
```
```   272   define iscale where [abs_def]: "iscale z = inverse 2 *\<^sub>R (z + 1)" for z :: real
```
```   273   have isc: "iscale ` {- 1..1} \<subseteq> {0..1}"
```
```   274     unfolding iscale_def by auto
```
```   275   have "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. (f \<circ> iscale) s = (g \<circ> iscale) t"
```
```   276   proof (rule fashoda_unit)
```
```   277     show "(f \<circ> iscale) ` {- 1..1} \<subseteq> cbox (- 1) 1" "(g \<circ> iscale) ` {- 1..1} \<subseteq> cbox (- 1) 1"
```
```   278       using isc and assms(3-4) by (auto simp add: image_comp [symmetric])
```
```   279     have *: "continuous_on {- 1..1} iscale"
```
```   280       unfolding iscale_def by (rule continuous_intros)+
```
```   281     show "continuous_on {- 1..1} (f \<circ> iscale)" "continuous_on {- 1..1} (g \<circ> iscale)"
```
```   282       apply -
```
```   283       apply (rule_tac[!] continuous_on_compose[OF *])
```
```   284       apply (rule_tac[!] continuous_on_subset[OF _ isc])
```
```   285       apply (rule assms)+
```
```   286       done
```
```   287     have *: "(1 / 2) *\<^sub>R (1 + (1::real^1)) = 1"
```
```   288       unfolding vec_eq_iff by auto
```
```   289     show "(f \<circ> iscale) (- 1) \$ 1 = - 1"
```
```   290       and "(f \<circ> iscale) 1 \$ 1 = 1"
```
```   291       and "(g \<circ> iscale) (- 1) \$ 2 = -1"
```
```   292       and "(g \<circ> iscale) 1 \$ 2 = 1"
```
```   293       unfolding o_def iscale_def
```
```   294       using assms
```
```   295       by (auto simp add: *)
```
```   296   qed
```
```   297   then obtain s t where st:
```
```   298       "s \<in> {- 1..1}"
```
```   299       "t \<in> {- 1..1}"
```
```   300       "(f \<circ> iscale) s = (g \<circ> iscale) t"
```
```   301     by auto
```
```   302   show thesis
```
```   303     apply (rule_tac z = "f (iscale s)" in that)
```
```   304     using st
```
```   305     unfolding o_def path_image_def image_iff
```
```   306     apply -
```
```   307     apply (rule_tac x="iscale s" in bexI)
```
```   308     prefer 3
```
```   309     apply (rule_tac x="iscale t" in bexI)
```
```   310     using isc[unfolded subset_eq, rule_format]
```
```   311     apply auto
```
```   312     done
```
```   313 qed
```
```   314
```
```   315 theorem fashoda:
```
```   316   fixes b :: "real^2"
```
```   317   assumes "path f"
```
```   318     and "path g"
```
```   319     and "path_image f \<subseteq> cbox a b"
```
```   320     and "path_image g \<subseteq> cbox a b"
```
```   321     and "(pathstart f)\$1 = a\$1"
```
```   322     and "(pathfinish f)\$1 = b\$1"
```
```   323     and "(pathstart g)\$2 = a\$2"
```
```   324     and "(pathfinish g)\$2 = b\$2"
```
```   325   obtains z where "z \<in> path_image f" and "z \<in> path_image g"
```
```   326 proof -
```
```   327   fix P Q S
```
```   328   presume "P \<or> Q \<or> S" "P \<Longrightarrow> thesis" and "Q \<Longrightarrow> thesis" and "S \<Longrightarrow> thesis"
```
```   329   then show thesis
```
```   330     by auto
```
```   331 next
```
```   332   have "cbox a b \<noteq> {}"
```
```   333     using assms(3) using path_image_nonempty[of f] by auto
```
```   334   then have "a \<le> b"
```
```   335     unfolding interval_eq_empty_cart less_eq_vec_def by (auto simp add: not_less)
```
```   336   then show "a\$1 = b\$1 \<or> a\$2 = b\$2 \<or> (a\$1 < b\$1 \<and> a\$2 < b\$2)"
```
```   337     unfolding less_eq_vec_def forall_2 by auto
```
```   338 next
```
```   339   assume as: "a\$1 = b\$1"
```
```   340   have "\<exists>z\<in>path_image g. z\$2 = (pathstart f)\$2"
```
```   341     apply (rule connected_ivt_component_cart)
```
```   342     apply (rule connected_path_image assms)+
```
```   343     apply (rule pathstart_in_path_image)
```
```   344     apply (rule pathfinish_in_path_image)
```
```   345     unfolding assms using assms(3)[unfolded path_image_def subset_eq,rule_format,of "f 0"]
```
```   346     unfolding pathstart_def
```
```   347     apply (auto simp add: less_eq_vec_def mem_box_cart)
```
```   348     done
```
```   349   then obtain z :: "real^2" where z: "z \<in> path_image g" "z \$ 2 = pathstart f \$ 2" ..
```
```   350   have "z \<in> cbox a b"
```
```   351     using z(1) assms(4)
```
```   352     unfolding path_image_def
```
```   353     by blast
```
```   354   then have "z = f 0"
```
```   355     unfolding vec_eq_iff forall_2
```
```   356     unfolding z(2) pathstart_def
```
```   357     using assms(3)[unfolded path_image_def subset_eq mem_box_cart,rule_format,of "f 0" 1]
```
```   358     unfolding mem_box_cart
```
```   359     apply (erule_tac x=1 in allE)
```
```   360     using as
```
```   361     apply auto
```
```   362     done
```
```   363   then show thesis
```
```   364     apply -
```
```   365     apply (rule that[OF _ z(1)])
```
```   366     unfolding path_image_def
```
```   367     apply auto
```
```   368     done
```
```   369 next
```
```   370   assume as: "a\$2 = b\$2"
```
```   371   have "\<exists>z\<in>path_image f. z\$1 = (pathstart g)\$1"
```
```   372     apply (rule connected_ivt_component_cart)
```
```   373     apply (rule connected_path_image assms)+
```
```   374     apply (rule pathstart_in_path_image)
```
```   375     apply (rule pathfinish_in_path_image)
```
```   376     unfolding assms
```
```   377     using assms(4)[unfolded path_image_def subset_eq,rule_format,of "g 0"]
```
```   378     unfolding pathstart_def
```
```   379     apply (auto simp add: less_eq_vec_def mem_box_cart)
```
```   380     done
```
```   381   then obtain z where z: "z \<in> path_image f" "z \$ 1 = pathstart g \$ 1" ..
```
```   382   have "z \<in> cbox a b"
```
```   383     using z(1) assms(3)
```
```   384     unfolding path_image_def
```
```   385     by blast
```
```   386   then have "z = g 0"
```
```   387     unfolding vec_eq_iff forall_2
```
```   388     unfolding z(2) pathstart_def
```
```   389     using assms(4)[unfolded path_image_def subset_eq mem_box_cart,rule_format,of "g 0" 2]
```
```   390     unfolding mem_box_cart
```
```   391     apply (erule_tac x=2 in allE)
```
```   392     using as
```
```   393     apply auto
```
```   394     done
```
```   395   then show thesis
```
```   396     apply -
```
```   397     apply (rule that[OF z(1)])
```
```   398     unfolding path_image_def
```
```   399     apply auto
```
```   400     done
```
```   401 next
```
```   402   assume as: "a \$ 1 < b \$ 1 \<and> a \$ 2 < b \$ 2"
```
```   403   have int_nem: "cbox (-1) (1::real^2) \<noteq> {}"
```
```   404     unfolding interval_eq_empty_cart by auto
```
```   405   obtain z :: "real^2" where z:
```
```   406       "z \<in> (interval_bij (a, b) (- 1, 1) \<circ> f) ` {0..1}"
```
```   407       "z \<in> (interval_bij (a, b) (- 1, 1) \<circ> g) ` {0..1}"
```
```   408     apply (rule fashoda_unit_path[of "interval_bij (a,b) (- 1,1) \<circ> f" "interval_bij (a,b) (- 1,1) \<circ> g"])
```
```   409     unfolding path_def path_image_def pathstart_def pathfinish_def
```
```   410     apply (rule_tac[1-2] continuous_on_compose)
```
```   411     apply (rule assms[unfolded path_def] continuous_on_interval_bij)+
```
```   412     unfolding subset_eq
```
```   413     apply(rule_tac[1-2] ballI)
```
```   414   proof -
```
```   415     fix x
```
```   416     assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> f) ` {0..1}"
```
```   417     then obtain y where y:
```
```   418         "y \<in> {0..1}"
```
```   419         "x = (interval_bij (a, b) (- 1, 1) \<circ> f) y"
```
```   420       unfolding image_iff ..
```
```   421     show "x \<in> cbox (- 1) 1"
```
```   422       unfolding y o_def
```
```   423       apply (rule in_interval_interval_bij)
```
```   424       using y(1)
```
```   425       using assms(3)[unfolded path_image_def subset_eq] int_nem
```
```   426       apply auto
```
```   427       done
```
```   428   next
```
```   429     fix x
```
```   430     assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> g) ` {0..1}"
```
```   431     then obtain y where y:
```
```   432         "y \<in> {0..1}"
```
```   433         "x = (interval_bij (a, b) (- 1, 1) \<circ> g) y"
```
```   434       unfolding image_iff ..
```
```   435     show "x \<in> cbox (- 1) 1"
```
```   436       unfolding y o_def
```
```   437       apply (rule in_interval_interval_bij)
```
```   438       using y(1)
```
```   439       using assms(4)[unfolded path_image_def subset_eq] int_nem
```
```   440       apply auto
```
```   441       done
```
```   442   next
```
```   443     show "(interval_bij (a, b) (- 1, 1) \<circ> f) 0 \$ 1 = -1"
```
```   444       and "(interval_bij (a, b) (- 1, 1) \<circ> f) 1 \$ 1 = 1"
```
```   445       and "(interval_bij (a, b) (- 1, 1) \<circ> g) 0 \$ 2 = -1"
```
```   446       and "(interval_bij (a, b) (- 1, 1) \<circ> g) 1 \$ 2 = 1"
```
```   447       using assms as
```
```   448       by (simp_all add: cart_eq_inner_axis pathstart_def pathfinish_def interval_bij_def)
```
```   449          (simp_all add: inner_axis)
```
```   450   qed
```
```   451   from z(1) obtain zf where zf:
```
```   452       "zf \<in> {0..1}"
```
```   453       "z = (interval_bij (a, b) (- 1, 1) \<circ> f) zf"
```
```   454     unfolding image_iff ..
```
```   455   from z(2) obtain zg where zg:
```
```   456       "zg \<in> {0..1}"
```
```   457       "z = (interval_bij (a, b) (- 1, 1) \<circ> g) zg"
```
```   458     unfolding image_iff ..
```
```   459   have *: "\<forall>i. (- 1) \$ i < (1::real^2) \$ i \<and> a \$ i < b \$ i"
```
```   460     unfolding forall_2
```
```   461     using as
```
```   462     by auto
```
```   463   show thesis
```
```   464   proof (rule_tac z="interval_bij (- 1,1) (a,b) z" in that)
```
```   465     show "interval_bij (- 1, 1) (a, b) z \<in> path_image f"
```
```   466       using zf by (simp add: interval_bij_bij_cart[OF *] path_image_def)
```
```   467     show "interval_bij (- 1, 1) (a, b) z \<in> path_image g"
```
```   468       using zg by (simp add: interval_bij_bij_cart[OF *] path_image_def)
```
```   469   qed
```
```   470 qed
```
```   471
```
```   472
```
```   473 subsection%unimportant \<open>Some slightly ad hoc lemmas I use below\<close>
```
```   474
```
```   475 lemma segment_vertical:
```
```   476   fixes a :: "real^2"
```
```   477   assumes "a\$1 = b\$1"
```
```   478   shows "x \<in> closed_segment a b \<longleftrightarrow>
```
```   479     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)"
```
```   480   (is "_ = ?R")
```
```   481 proof -
```
```   482   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"
```
```   483   {
```
```   484     presume "?L \<Longrightarrow> ?R" and "?R \<Longrightarrow> ?L"
```
```   485     then show ?thesis
```
```   486       unfolding closed_segment_def mem_Collect_eq
```
```   487       unfolding vec_eq_iff forall_2 scalar_mult_eq_scaleR[symmetric] vector_component_simps
```
```   488       by blast
```
```   489   }
```
```   490   {
```
```   491     assume ?L
```
```   492     then obtain u where u:
```
```   493         "x \$ 1 = (1 - u) * a \$ 1 + u * b \$ 1"
```
```   494         "x \$ 2 = (1 - u) * a \$ 2 + u * b \$ 2"
```
```   495         "0 \<le> u"
```
```   496         "u \<le> 1"
```
```   497       by blast
```
```   498     { fix b a
```
```   499       assume "b + u * a > a + u * b"
```
```   500       then have "(1 - u) * b > (1 - u) * a"
```
```   501         by (auto simp add:field_simps)
```
```   502       then have "b \<ge> a"
```
```   503         apply (drule_tac mult_left_less_imp_less)
```
```   504         using u
```
```   505         apply auto
```
```   506         done
```
```   507       then have "u * a \<le> u * b"
```
```   508         apply -
```
```   509         apply (rule mult_left_mono[OF _ u(3)])
```
```   510         using u(3-4)
```
```   511         apply (auto simp add: field_simps)
```
```   512         done
```
```   513     } note * = this
```
```   514     {
```
```   515       fix a b
```
```   516       assume "u * b > u * a"
```
```   517       then have "(1 - u) * a \<le> (1 - u) * b"
```
```   518         apply -
```
```   519         apply (rule mult_left_mono)
```
```   520         apply (drule mult_left_less_imp_less)
```
```   521         using u
```
```   522         apply auto
```
```   523         done
```
```   524       then have "a + u * b \<le> b + u * a"
```
```   525         by (auto simp add: field_simps)
```
```   526     } note ** = this
```
```   527     then show ?R
```
```   528       unfolding u assms
```
```   529       using u
```
```   530       by (auto simp add:field_simps not_le intro: * **)
```
```   531   }
```
```   532   {
```
```   533     assume ?R
```
```   534     then show ?L
```
```   535     proof (cases "x\$2 = b\$2")
```
```   536       case True
```
```   537       then show ?L
```
```   538         apply (rule_tac x="(x\$2 - a\$2) / (b\$2 - a\$2)" in exI)
```
```   539         unfolding assms True using \<open>?R\<close> apply (auto simp add: field_simps)
```
```   540         done
```
```   541     next
```
```   542       case False
```
```   543       then show ?L
```
```   544         apply (rule_tac x="1 - (x\$2 - b\$2) / (a\$2 - b\$2)" in exI)
```
```   545         unfolding assms using \<open>?R\<close> apply (auto simp add: field_simps)
```
```   546         done
```
```   547     qed
```
```   548   }
```
```   549 qed
```
```   550
```
```   551 lemma segment_horizontal:
```
```   552   fixes a :: "real^2"
```
```   553   assumes "a\$2 = b\$2"
```
```   554   shows "x \<in> closed_segment a b \<longleftrightarrow>
```
```   555     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)"
```
```   556   (is "_ = ?R")
```
```   557 proof -
```
```   558   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"
```
```   559   {
```
```   560     presume "?L \<Longrightarrow> ?R" and "?R \<Longrightarrow> ?L"
```
```   561     then show ?thesis
```
```   562       unfolding closed_segment_def mem_Collect_eq
```
```   563       unfolding vec_eq_iff forall_2 scalar_mult_eq_scaleR[symmetric] vector_component_simps
```
```   564       by blast
```
```   565   }
```
```   566   {
```
```   567     assume ?L
```
```   568     then obtain u where u:
```
```   569         "x \$ 1 = (1 - u) * a \$ 1 + u * b \$ 1"
```
```   570         "x \$ 2 = (1 - u) * a \$ 2 + u * b \$ 2"
```
```   571         "0 \<le> u"
```
```   572         "u \<le> 1"
```
```   573       by blast
```
```   574     {
```
```   575       fix b a
```
```   576       assume "b + u * a > a + u * b"
```
```   577       then have "(1 - u) * b > (1 - u) * a"
```
```   578         by (auto simp add: field_simps)
```
```   579       then have "b \<ge> a"
```
```   580         apply (drule_tac mult_left_less_imp_less)
```
```   581         using u
```
```   582         apply auto
```
```   583         done
```
```   584       then have "u * a \<le> u * b"
```
```   585         apply -
```
```   586         apply (rule mult_left_mono[OF _ u(3)])
```
```   587         using u(3-4)
```
```   588         apply (auto simp add: field_simps)
```
```   589         done
```
```   590     } note * = this
```
```   591     {
```
```   592       fix a b
```
```   593       assume "u * b > u * a"
```
```   594       then have "(1 - u) * a \<le> (1 - u) * b"
```
```   595         apply -
```
```   596         apply (rule mult_left_mono)
```
```   597         apply (drule mult_left_less_imp_less)
```
```   598         using u
```
```   599         apply auto
```
```   600         done
```
```   601       then have "a + u * b \<le> b + u * a"
```
```   602         by (auto simp add: field_simps)
```
```   603     } note ** = this
```
```   604     then show ?R
```
```   605       unfolding u assms
```
```   606       using u
```
```   607       by (auto simp add: field_simps not_le intro: * **)
```
```   608   }
```
```   609   {
```
```   610     assume ?R
```
```   611     then show ?L
```
```   612     proof (cases "x\$1 = b\$1")
```
```   613       case True
```
```   614       then show ?L
```
```   615         apply (rule_tac x="(x\$1 - a\$1) / (b\$1 - a\$1)" in exI)
```
```   616         unfolding assms True
```
```   617         using \<open>?R\<close>
```
```   618         apply (auto simp add: field_simps)
```
```   619         done
```
```   620     next
```
```   621       case False
```
```   622       then show ?L
```
```   623         apply (rule_tac x="1 - (x\$1 - b\$1) / (a\$1 - b\$1)" in exI)
```
```   624         unfolding assms
```
```   625         using \<open>?R\<close>
```
```   626         apply (auto simp add: field_simps)
```
```   627         done
```
```   628     qed
```
```   629   }
```
```   630 qed
```
```   631
```
```   632
```
```   633 subsection \<open>Useful Fashoda corollary pointed out to me by Tom Hales\<close>(*FIXME change title? *)
```
```   634
```
```   635 corollary fashoda_interlace:
```
```   636   fixes a :: "real^2"
```
```   637   assumes "path f"
```
```   638     and "path g"
```
```   639     and paf: "path_image f \<subseteq> cbox a b"
```
```   640     and pag: "path_image g \<subseteq> cbox a b"
```
```   641     and "(pathstart f)\$2 = a\$2"
```
```   642     and "(pathfinish f)\$2 = a\$2"
```
```   643     and "(pathstart g)\$2 = a\$2"
```
```   644     and "(pathfinish g)\$2 = a\$2"
```
```   645     and "(pathstart f)\$1 < (pathstart g)\$1"
```
```   646     and "(pathstart g)\$1 < (pathfinish f)\$1"
```
```   647     and "(pathfinish f)\$1 < (pathfinish g)\$1"
```
```   648   obtains z where "z \<in> path_image f" and "z \<in> path_image g"
```
```   649 proof -
```
```   650   have "cbox a b \<noteq> {}"
```
```   651     using path_image_nonempty[of f] using assms(3) by auto
```
```   652   note ab=this[unfolded interval_eq_empty_cart not_ex forall_2 not_less]
```
```   653   have "pathstart f \<in> cbox a b"
```
```   654     and "pathfinish f \<in> cbox a b"
```
```   655     and "pathstart g \<in> cbox a b"
```
```   656     and "pathfinish g \<in> cbox a b"
```
```   657     using pathstart_in_path_image pathfinish_in_path_image
```
```   658     using assms(3-4)
```
```   659     by auto
```
```   660   note startfin = this[unfolded mem_box_cart forall_2]
```
```   661   let ?P1 = "linepath (vector[a\$1 - 2, a\$2 - 2]) (vector[(pathstart f)\$1,a\$2 - 2]) +++
```
```   662      linepath(vector[(pathstart f)\$1,a\$2 - 2])(pathstart f) +++ f +++
```
```   663      linepath(pathfinish f)(vector[(pathfinish f)\$1,a\$2 - 2]) +++
```
```   664      linepath(vector[(pathfinish f)\$1,a\$2 - 2])(vector[b\$1 + 2,a\$2 - 2])"
```
```   665   let ?P2 = "linepath(vector[(pathstart g)\$1, (pathstart g)\$2 - 3])(pathstart g) +++ g +++
```
```   666      linepath(pathfinish g)(vector[(pathfinish g)\$1,a\$2 - 1]) +++
```
```   667      linepath(vector[(pathfinish g)\$1,a\$2 - 1])(vector[b\$1 + 1,a\$2 - 1]) +++
```
```   668      linepath(vector[b\$1 + 1,a\$2 - 1])(vector[b\$1 + 1,b\$2 + 3])"
```
```   669   let ?a = "vector[a\$1 - 2, a\$2 - 3]"
```
```   670   let ?b = "vector[b\$1 + 2, b\$2 + 3]"
```
```   671   have P1P2: "path_image ?P1 = path_image (linepath (vector[a\$1 - 2, a\$2 - 2]) (vector[(pathstart f)\$1,a\$2 - 2])) \<union>
```
```   672       path_image (linepath(vector[(pathstart f)\$1,a\$2 - 2])(pathstart f)) \<union> path_image f \<union>
```
```   673       path_image (linepath(pathfinish f)(vector[(pathfinish f)\$1,a\$2 - 2])) \<union>
```
```   674       path_image (linepath(vector[(pathfinish f)\$1,a\$2 - 2])(vector[b\$1 + 2,a\$2 - 2]))"
```
```   675     "path_image ?P2 = path_image(linepath(vector[(pathstart g)\$1, (pathstart g)\$2 - 3])(pathstart g)) \<union> path_image g \<union>
```
```   676       path_image(linepath(pathfinish g)(vector[(pathfinish g)\$1,a\$2 - 1])) \<union>
```
```   677       path_image(linepath(vector[(pathfinish g)\$1,a\$2 - 1])(vector[b\$1 + 1,a\$2 - 1])) \<union>
```
```   678       path_image(linepath(vector[b\$1 + 1,a\$2 - 1])(vector[b\$1 + 1,b\$2 + 3]))" using assms(1-2)
```
```   679       by(auto simp add: path_image_join path_linepath)
```
```   680   have abab: "cbox a b \<subseteq> cbox ?a ?b"
```
```   681     unfolding interval_cbox_cart[symmetric]
```
```   682     by (auto simp add:less_eq_vec_def forall_2 vector_2)
```
```   683   obtain z where
```
```   684     "z \<in> path_image
```
```   685           (linepath (vector [a \$ 1 - 2, a \$ 2 - 2]) (vector [pathstart f \$ 1, a \$ 2 - 2]) +++
```
```   686            linepath (vector [pathstart f \$ 1, a \$ 2 - 2]) (pathstart f) +++
```
```   687            f +++
```
```   688            linepath (pathfinish f) (vector [pathfinish f \$ 1, a \$ 2 - 2]) +++
```
```   689            linepath (vector [pathfinish f \$ 1, a \$ 2 - 2]) (vector [b \$ 1 + 2, a \$ 2 - 2]))"
```
```   690     "z \<in> path_image
```
```   691           (linepath (vector [pathstart g \$ 1, pathstart g \$ 2 - 3]) (pathstart g) +++
```
```   692            g +++
```
```   693            linepath (pathfinish g) (vector [pathfinish g \$ 1, a \$ 2 - 1]) +++
```
```   694            linepath (vector [pathfinish g \$ 1, a \$ 2 - 1]) (vector [b \$ 1 + 1, a \$ 2 - 1]) +++
```
```   695            linepath (vector [b \$ 1 + 1, a \$ 2 - 1]) (vector [b \$ 1 + 1, b \$ 2 + 3]))"
```
```   696     apply (rule fashoda[of ?P1 ?P2 ?a ?b])
```
```   697     unfolding pathstart_join pathfinish_join pathstart_linepath pathfinish_linepath vector_2
```
```   698   proof -
```
```   699     show "path ?P1" and "path ?P2"
```
```   700       using assms by auto
```
```   701     show "path_image ?P1 \<subseteq> cbox ?a ?b" "path_image ?P2 \<subseteq> cbox ?a ?b"
```
```   702       unfolding P1P2 path_image_linepath using startfin paf pag
```
```   703       by (auto simp: mem_box_cart segment_horizontal segment_vertical forall_2)
```
```   704     show "a \$ 1 - 2 = a \$ 1 - 2"
```
```   705       and "b \$ 1 + 2 = b \$ 1 + 2"
```
```   706       and "pathstart g \$ 2 - 3 = a \$ 2 - 3"
```
```   707       and "b \$ 2 + 3 = b \$ 2 + 3"
```
```   708       by (auto simp add: assms)
```
```   709   qed
```
```   710   note z=this[unfolded P1P2 path_image_linepath]
```
```   711   show thesis
```
```   712   proof (rule that[of z])
```
```   713     have "(z \<in> closed_segment (vector [a \$ 1 - 2, a \$ 2 - 2]) (vector [pathstart f \$ 1, a \$ 2 - 2]) \<or>
```
```   714       z \<in> closed_segment (vector [pathstart f \$ 1, a \$ 2 - 2]) (pathstart f)) \<or>
```
```   715       z \<in> closed_segment (pathfinish f) (vector [pathfinish f \$ 1, a \$ 2 - 2]) \<or>
```
```   716       z \<in> closed_segment (vector [pathfinish f \$ 1, a \$ 2 - 2]) (vector [b \$ 1 + 2, a \$ 2 - 2]) \<Longrightarrow>
```
```   717     (((z \<in> closed_segment (vector [pathstart g \$ 1, pathstart g \$ 2 - 3]) (pathstart g)) \<or>
```
```   718       z \<in> closed_segment (pathfinish g) (vector [pathfinish g \$ 1, a \$ 2 - 1])) \<or>
```
```   719       z \<in> closed_segment (vector [pathfinish g \$ 1, a \$ 2 - 1]) (vector [b \$ 1 + 1, a \$ 2 - 1])) \<or>
```
```   720       z \<in> closed_segment (vector [b \$ 1 + 1, a \$ 2 - 1]) (vector [b \$ 1 + 1, b \$ 2 + 3]) \<Longrightarrow> False"
```
```   721     proof (simp only: segment_vertical segment_horizontal vector_2, goal_cases)
```
```   722       case prems: 1
```
```   723       have "pathfinish f \<in> cbox a b"
```
```   724         using assms(3) pathfinish_in_path_image[of f] by auto
```
```   725       then have "1 + b \$ 1 \<le> pathfinish f \$ 1 \<Longrightarrow> False"
```
```   726         unfolding mem_box_cart forall_2 by auto
```
```   727       then have "z\$1 \<noteq> pathfinish f\$1"
```
```   728         using prems(2)
```
```   729         using assms ab
```
```   730         by (auto simp add: field_simps)
```
```   731       moreover have "pathstart f \<in> cbox a b"
```
```   732         using assms(3) pathstart_in_path_image[of f]
```
```   733         by auto
```
```   734       then have "1 + b \$ 1 \<le> pathstart f \$ 1 \<Longrightarrow> False"
```
```   735         unfolding mem_box_cart forall_2
```
```   736         by auto
```
```   737       then have "z\$1 \<noteq> pathstart f\$1"
```
```   738         using prems(2) using assms ab
```
```   739         by (auto simp add: field_simps)
```
```   740       ultimately have *: "z\$2 = a\$2 - 2"
```
```   741         using prems(1) by auto
```
```   742       have "z\$1 \<noteq> pathfinish g\$1"
```
```   743         using prems(2) assms ab
```
```   744         by (auto simp add: field_simps *)
```
```   745       moreover have "pathstart g \<in> cbox a b"
```
```   746         using assms(4) pathstart_in_path_image[of g]
```
```   747         by auto
```
```   748       note this[unfolded mem_box_cart forall_2]
```
```   749       then have "z\$1 \<noteq> pathstart g\$1"
```
```   750         using prems(1) assms ab
```
```   751         by (auto simp add: field_simps *)
```
```   752       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"
```
```   753         using prems(2)  unfolding * assms by (auto simp add: field_simps)
```
```   754       then show False
```
```   755         unfolding * using ab by auto
```
```   756     qed
```
```   757     then have "z \<in> path_image f \<or> z \<in> path_image g"
```
```   758       using z unfolding Un_iff by blast
```
```   759     then have z': "z \<in> cbox a b"
```
```   760       using assms(3-4) by auto
```
```   761     have "a \$ 2 = z \$ 2 \<Longrightarrow> (z \$ 1 = pathstart f \$ 1 \<or> z \$ 1 = pathfinish f \$ 1) \<Longrightarrow>
```
```   762       z = pathstart f \<or> z = pathfinish f"
```
```   763       unfolding vec_eq_iff forall_2 assms
```
```   764       by auto
```
```   765     with z' show "z \<in> path_image f"
```
```   766       using z(1)
```
```   767       unfolding Un_iff mem_box_cart forall_2
```
```   768       by (simp only: segment_vertical segment_horizontal vector_2) (auto simp: assms)
```
```   769     have "a \$ 2 = z \$ 2 \<Longrightarrow> (z \$ 1 = pathstart g \$ 1 \<or> z \$ 1 = pathfinish g \$ 1) \<Longrightarrow>
```
```   770       z = pathstart g \<or> z = pathfinish g"
```
```   771       unfolding vec_eq_iff forall_2 assms
```
```   772       by auto
```
```   773     with z' show "z \<in> path_image g"
```
```   774       using z(2)
```
```   775       unfolding Un_iff mem_box_cart forall_2
```
```   776       by (simp only: segment_vertical segment_horizontal vector_2) (auto simp: assms)
```
```   777   qed
```
```   778 qed
```
```   779
```
```   780 end
```