173 done |
173 done |
174 qed |
174 qed |
175 qed |
175 qed |
176 have 3: "(negatex \<circ> sqprojection \<circ> ?F) ` cbox (-1) 1 \<subseteq> cbox (-1) 1" |
176 have 3: "(negatex \<circ> sqprojection \<circ> ?F) ` cbox (-1) 1 \<subseteq> cbox (-1) 1" |
177 unfolding subset_eq |
177 unfolding subset_eq |
178 proof (rule, goals) |
178 proof (rule, goal_cases) |
179 case (1 x) |
179 case (1 x) |
180 then obtain y :: "real^2" where y: |
180 then obtain y :: "real^2" where y: |
181 "y \<in> cbox (- 1) 1" |
181 "y \<in> cbox (- 1) 1" |
182 "x = (negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w)) y" |
182 "x = (negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w)) y" |
183 unfolding image_iff .. |
183 unfolding image_iff .. |
832 z \<in> closed_segment (vector [pathfinish f $ 1, a $ 2 - 2]) (vector [b $ 1 + 2, a $ 2 - 2]) \<Longrightarrow> |
832 z \<in> closed_segment (vector [pathfinish f $ 1, a $ 2 - 2]) (vector [b $ 1 + 2, a $ 2 - 2]) \<Longrightarrow> |
833 (((z \<in> closed_segment (vector [pathstart g $ 1, pathstart g $ 2 - 3]) (pathstart g)) \<or> |
833 (((z \<in> closed_segment (vector [pathstart g $ 1, pathstart g $ 2 - 3]) (pathstart g)) \<or> |
834 z \<in> closed_segment (pathfinish g) (vector [pathfinish g $ 1, a $ 2 - 1])) \<or> |
834 z \<in> closed_segment (pathfinish g) (vector [pathfinish g $ 1, a $ 2 - 1])) \<or> |
835 z \<in> closed_segment (vector [pathfinish g $ 1, a $ 2 - 1]) (vector [b $ 1 + 1, a $ 2 - 1])) \<or> |
835 z \<in> closed_segment (vector [pathfinish g $ 1, a $ 2 - 1]) (vector [b $ 1 + 1, a $ 2 - 1])) \<or> |
836 z \<in> closed_segment (vector [b $ 1 + 1, a $ 2 - 1]) (vector [b $ 1 + 1, b $ 2 + 3]) \<Longrightarrow> False" |
836 z \<in> closed_segment (vector [b $ 1 + 1, a $ 2 - 1]) (vector [b $ 1 + 1, b $ 2 + 3]) \<Longrightarrow> False" |
837 proof (simp only: segment_vertical segment_horizontal vector_2, goals) |
837 proof (simp only: segment_vertical segment_horizontal vector_2, goal_cases) |
838 case as: 1 |
838 case as: 1 |
839 have "pathfinish f \<in> cbox a b" |
839 have "pathfinish f \<in> cbox a b" |
840 using assms(3) pathfinish_in_path_image[of f] by auto |
840 using assms(3) pathfinish_in_path_image[of f] by auto |
841 then have "1 + b $ 1 \<le> pathfinish f $ 1 \<Longrightarrow> False" |
841 then have "1 + b $ 1 \<le> pathfinish f $ 1 \<Longrightarrow> False" |
842 unfolding mem_interval_cart forall_2 by auto |
842 unfolding mem_interval_cart forall_2 by auto |