equal
deleted
inserted
replaced
144 } note x0 = this |
144 } note x0 = this |
145 have 21: "\<And>i::2. i \<noteq> 1 \<Longrightarrow> i = 2" |
145 have 21: "\<And>i::2. i \<noteq> 1 \<Longrightarrow> i = 2" |
146 using UNIV_2 by auto |
146 using UNIV_2 by auto |
147 have 1: "box (- 1) (1::real^2) \<noteq> {}" |
147 have 1: "box (- 1) (1::real^2) \<noteq> {}" |
148 unfolding interval_eq_empty_cart by auto |
148 unfolding interval_eq_empty_cart by auto |
149 have 2: "continuous_on (cbox -1 1) (negatex \<circ> sqprojection \<circ> ?F)" |
149 have 2: "continuous_on (cbox (- 1) 1) (negatex \<circ> sqprojection \<circ> ?F)" |
150 apply (intro continuous_intros continuous_on_component) |
150 apply (intro continuous_intros continuous_on_component) |
151 unfolding * |
151 unfolding * |
152 apply (rule assms)+ |
152 apply (rule assms)+ |
153 apply (subst sqprojection_def) |
153 apply (subst sqprojection_def) |
154 apply (intro continuous_intros) |
154 apply (intro continuous_intros) |
177 unfolding subset_eq |
177 unfolding subset_eq |
178 apply rule |
178 apply rule |
179 proof - |
179 proof - |
180 case goal1 |
180 case goal1 |
181 then obtain y :: "real^2" where y: |
181 then obtain y :: "real^2" where y: |
182 "y \<in> cbox -1 1" |
182 "y \<in> cbox (- 1) 1" |
183 "x = (negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w)) y" |
183 "x = (negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w)) y" |
184 unfolding image_iff .. |
184 unfolding image_iff .. |
185 have "?F y \<noteq> 0" |
185 have "?F y \<noteq> 0" |
186 apply (rule x0) |
186 apply (rule x0) |
187 using y(1) |
187 using y(1) |
206 apply auto |
206 apply auto |
207 done |
207 done |
208 qed |
208 qed |
209 qed |
209 qed |
210 obtain x :: "real^2" where x: |
210 obtain x :: "real^2" where x: |
211 "x \<in> cbox -1 1" |
211 "x \<in> cbox (- 1) 1" |
212 "(negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w)) x = x" |
212 "(negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w)) x = x" |
213 apply (rule brouwer_weak[of "cbox -1 (1::real^2)" "negatex \<circ> sqprojection \<circ> ?F"]) |
213 apply (rule brouwer_weak[of "cbox (- 1) (1::real^2)" "negatex \<circ> sqprojection \<circ> ?F"]) |
214 apply (rule compact_cbox convex_box)+ |
214 apply (rule compact_cbox convex_box)+ |
215 unfolding interior_cbox |
215 unfolding interior_cbox |
216 apply (rule 1 2 3)+ |
216 apply (rule 1 2 3)+ |
217 apply blast |
217 apply blast |
218 done |
218 done |
360 def iscale \<equiv> "\<lambda>z::real. inverse 2 *\<^sub>R (z + 1)" |
360 def iscale \<equiv> "\<lambda>z::real. inverse 2 *\<^sub>R (z + 1)" |
361 have isc: "iscale ` {- 1..1} \<subseteq> {0..1}" |
361 have isc: "iscale ` {- 1..1} \<subseteq> {0..1}" |
362 unfolding iscale_def by auto |
362 unfolding iscale_def by auto |
363 have "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. (f \<circ> iscale) s = (g \<circ> iscale) t" |
363 have "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. (f \<circ> iscale) s = (g \<circ> iscale) t" |
364 proof (rule fashoda_unit) |
364 proof (rule fashoda_unit) |
365 show "(f \<circ> iscale) ` {- 1..1} \<subseteq> cbox -1 1" "(g \<circ> iscale) ` {- 1..1} \<subseteq> cbox -1 1" |
365 show "(f \<circ> iscale) ` {- 1..1} \<subseteq> cbox (- 1) 1" "(g \<circ> iscale) ` {- 1..1} \<subseteq> cbox (- 1) 1" |
366 using isc and assms(3-4) by (auto simp add: image_comp [symmetric]) |
366 using isc and assms(3-4) by (auto simp add: image_comp [symmetric]) |
367 have *: "continuous_on {- 1..1} iscale" |
367 have *: "continuous_on {- 1..1} iscale" |
368 unfolding iscale_def by (rule continuous_intros)+ |
368 unfolding iscale_def by (rule continuous_intros)+ |
369 show "continuous_on {- 1..1} (f \<circ> iscale)" "continuous_on {- 1..1} (g \<circ> iscale)" |
369 show "continuous_on {- 1..1} (f \<circ> iscale)" "continuous_on {- 1..1} (g \<circ> iscale)" |
370 apply - |
370 apply - |
504 assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> f) ` {0..1}" |
504 assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> f) ` {0..1}" |
505 then obtain y where y: |
505 then obtain y where y: |
506 "y \<in> {0..1}" |
506 "y \<in> {0..1}" |
507 "x = (interval_bij (a, b) (- 1, 1) \<circ> f) y" |
507 "x = (interval_bij (a, b) (- 1, 1) \<circ> f) y" |
508 unfolding image_iff .. |
508 unfolding image_iff .. |
509 show "x \<in> cbox -1 1" |
509 show "x \<in> cbox (- 1) 1" |
510 unfolding y o_def |
510 unfolding y o_def |
511 apply (rule in_interval_interval_bij) |
511 apply (rule in_interval_interval_bij) |
512 using y(1) |
512 using y(1) |
513 using assms(3)[unfolded path_image_def subset_eq] int_nem |
513 using assms(3)[unfolded path_image_def subset_eq] int_nem |
514 apply auto |
514 apply auto |
518 assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> g) ` {0..1}" |
518 assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> g) ` {0..1}" |
519 then obtain y where y: |
519 then obtain y where y: |
520 "y \<in> {0..1}" |
520 "y \<in> {0..1}" |
521 "x = (interval_bij (a, b) (- 1, 1) \<circ> g) y" |
521 "x = (interval_bij (a, b) (- 1, 1) \<circ> g) y" |
522 unfolding image_iff .. |
522 unfolding image_iff .. |
523 show "x \<in> cbox -1 1" |
523 show "x \<in> cbox (- 1) 1" |
524 unfolding y o_def |
524 unfolding y o_def |
525 apply (rule in_interval_interval_bij) |
525 apply (rule in_interval_interval_bij) |
526 using y(1) |
526 using y(1) |
527 using assms(4)[unfolded path_image_def subset_eq] int_nem |
527 using assms(4)[unfolded path_image_def subset_eq] int_nem |
528 apply auto |
528 apply auto |