178 using y(1) using assms(4)[unfolded path_image_def subset_eq] int_nem by auto |
178 using y(1) using assms(4)[unfolded path_image_def subset_eq] int_nem by auto |
179 next show "(interval_bij (a, b) (- 1, 1) \<circ> f) 0 $ 1 = -1" |
179 next show "(interval_bij (a, b) (- 1, 1) \<circ> f) 0 $ 1 = -1" |
180 "(interval_bij (a, b) (- 1, 1) \<circ> f) 1 $ 1 = 1" |
180 "(interval_bij (a, b) (- 1, 1) \<circ> f) 1 $ 1 = 1" |
181 "(interval_bij (a, b) (- 1, 1) \<circ> g) 0 $ 2 = -1" |
181 "(interval_bij (a, b) (- 1, 1) \<circ> g) 0 $ 2 = -1" |
182 "(interval_bij (a, b) (- 1, 1) \<circ> g) 1 $ 2 = 1" |
182 "(interval_bij (a, b) (- 1, 1) \<circ> g) 1 $ 2 = 1" |
183 unfolding interval_bij_cart vec_lambda_beta vector_component_simps o_def split_conv |
183 unfolding interval_bij_cart vector_component_simps o_def split_conv |
184 unfolding assms[unfolded pathstart_def pathfinish_def] using as by auto qed note z=this |
184 unfolding assms[unfolded pathstart_def pathfinish_def] using as by auto qed note z=this |
185 from z(1) guess zf unfolding image_iff .. note zf=this |
185 from z(1) guess zf unfolding image_iff .. note zf=this |
186 from z(2) guess zg unfolding image_iff .. note zg=this |
186 from z(2) guess zg unfolding image_iff .. note zg=this |
187 have *:"\<forall>i. (- 1) $ i < (1::real^2) $ i \<and> a $ i < b $ i" unfolding forall_2 using as by auto |
187 have *:"\<forall>i. (- 1) $ i < (1::real^2) $ i \<and> a $ i < b $ i" unfolding forall_2 using as by auto |
188 show thesis apply(rule_tac z="interval_bij (- 1,1) (a,b) z" in that) |
188 show thesis apply(rule_tac z="interval_bij (- 1,1) (a,b) z" in that) |