753 and umin: "\<And>t. \<lbrakk>0 \<le> t; t \<le> 1; g t \<in> closure (- S)\<rbrakk> \<Longrightarrow> u \<le> t" |
753 and umin: "\<And>t. \<lbrakk>0 \<le> t; t \<le> 1; g t \<in> closure (- S)\<rbrakk> \<Longrightarrow> u \<le> t" |
754 using compact_attains_inf [OF com dis] by fastforce |
754 using compact_attains_inf [OF com dis] by fastforce |
755 then have umin': "\<And>t. \<lbrakk>0 \<le> t; t \<le> 1; t < u\<rbrakk> \<Longrightarrow> g t \<in> S" |
755 then have umin': "\<And>t. \<lbrakk>0 \<le> t; t \<le> 1; t < u\<rbrakk> \<Longrightarrow> g t \<in> S" |
756 using closure_def by fastforce |
756 using closure_def by fastforce |
757 { assume "u \<noteq> 0" |
757 { assume "u \<noteq> 0" |
758 then have "u > 0" using `0 \<le> u` by auto |
758 then have "u > 0" using \<open>0 \<le> u\<close> by auto |
759 { fix e::real assume "e > 0" |
759 { fix e::real assume "e > 0" |
760 obtain d where "d>0" and d: "\<And>x'. \<lbrakk>x' \<in> {0..1}; dist x' u < d\<rbrakk> \<Longrightarrow> dist (g x') (g u) < e" |
760 obtain d where "d>0" and d: "\<And>x'. \<lbrakk>x' \<in> {0..1}; dist x' u < d\<rbrakk> \<Longrightarrow> dist (g x') (g u) < e" |
761 using continuous_onD [OF gcon _ `e > 0`] `0 \<le> _` `_ \<le> 1` atLeastAtMost_iff by auto |
761 using continuous_onD [OF gcon _ \<open>e > 0\<close>] \<open>0 \<le> _\<close> \<open>_ \<le> 1\<close> atLeastAtMost_iff by auto |
762 have *: "dist (max 0 (u - d / 2)) u < d" |
762 have *: "dist (max 0 (u - d / 2)) u < d" |
763 using `0 \<le> u` `u \<le> 1` `d > 0` by (simp add: dist_real_def) |
763 using \<open>0 \<le> u\<close> \<open>u \<le> 1\<close> \<open>d > 0\<close> by (simp add: dist_real_def) |
764 have "\<exists>y\<in>S. dist y (g u) < e" |
764 have "\<exists>y\<in>S. dist y (g u) < e" |
765 using `0 < u` `u \<le> 1` `d > 0` |
765 using \<open>0 < u\<close> \<open>u \<le> 1\<close> \<open>d > 0\<close> |
766 by (force intro: d [OF _ *] umin') |
766 by (force intro: d [OF _ *] umin') |
767 } |
767 } |
768 then have "g u \<in> closure S" |
768 then have "g u \<in> closure S" |
769 by (simp add: frontier_def closure_approachable) |
769 by (simp add: frontier_def closure_approachable) |
770 } |
770 } |
771 then show ?thesis |
771 then show ?thesis |
772 apply (rule_tac u=u in that) |
772 apply (rule_tac u=u in that) |
773 apply (auto simp: `0 \<le> u` `u \<le> 1` gu interior_closure umin) |
773 apply (auto simp: \<open>0 \<le> u\<close> \<open>u \<le> 1\<close> gu interior_closure umin) |
774 using `_ \<le> 1` interior_closure umin apply fastforce |
774 using \<open>_ \<le> 1\<close> interior_closure umin apply fastforce |
775 done |
775 done |
776 qed |
776 qed |
777 |
777 |
778 lemma subpath_to_frontier_strong: |
778 lemma subpath_to_frontier_strong: |
779 assumes g: "path g" and "pathfinish g \<notin> S" |
779 assumes g: "path g" and "pathfinish g \<notin> S" |
783 obtain u where "0 \<le> u" "u \<le> 1" |
783 obtain u where "0 \<le> u" "u \<le> 1" |
784 and gxin: "\<And>x. 0 \<le> x \<and> x < u \<Longrightarrow> g x \<in> interior S" |
784 and gxin: "\<And>x. 0 \<le> x \<and> x < u \<Longrightarrow> g x \<in> interior S" |
785 and gunot: "(g u \<notin> interior S)" and u0: "(u = 0 \<or> g u \<in> closure S)" |
785 and gunot: "(g u \<notin> interior S)" and u0: "(u = 0 \<or> g u \<in> closure S)" |
786 using subpath_to_frontier_explicit [OF assms] by blast |
786 using subpath_to_frontier_explicit [OF assms] by blast |
787 show ?thesis |
787 show ?thesis |
788 apply (rule that [OF `0 \<le> u` `u \<le> 1`]) |
788 apply (rule that [OF \<open>0 \<le> u\<close> \<open>u \<le> 1\<close>]) |
789 apply (simp add: gunot) |
789 apply (simp add: gunot) |
790 using `0 \<le> u` u0 by (force simp: subpath_def gxin) |
790 using \<open>0 \<le> u\<close> u0 by (force simp: subpath_def gxin) |
791 qed |
791 qed |
792 |
792 |
793 lemma subpath_to_frontier: |
793 lemma subpath_to_frontier: |
794 assumes g: "path g" and g0: "pathstart g \<in> closure S" and g1: "pathfinish g \<notin> S" |
794 assumes g: "path g" and g0: "pathstart g \<in> closure S" and g1: "pathfinish g \<notin> S" |
795 obtains u where "0 \<le> u" "u \<le> 1" "g u \<in> frontier S" "(path_image(subpath 0 u g) - {g u}) \<subseteq> interior S" |
795 obtains u where "0 \<le> u" "u \<le> 1" "g u \<in> frontier S" "(path_image(subpath 0 u g) - {g u}) \<subseteq> interior S" |
798 and notin: "g u \<notin> interior S" |
798 and notin: "g u \<notin> interior S" |
799 and disj: "u = 0 \<or> |
799 and disj: "u = 0 \<or> |
800 (\<forall>x. 0 \<le> x \<and> x < 1 \<longrightarrow> subpath 0 u g x \<in> interior S) \<and> g u \<in> closure S" |
800 (\<forall>x. 0 \<le> x \<and> x < 1 \<longrightarrow> subpath 0 u g x \<in> interior S) \<and> g u \<in> closure S" |
801 using subpath_to_frontier_strong [OF g g1] by blast |
801 using subpath_to_frontier_strong [OF g g1] by blast |
802 show ?thesis |
802 show ?thesis |
803 apply (rule that [OF `0 \<le> u` `u \<le> 1`]) |
803 apply (rule that [OF \<open>0 \<le> u\<close> \<open>u \<le> 1\<close>]) |
804 apply (metis DiffI disj frontier_def g0 notin pathstart_def) |
804 apply (metis DiffI disj frontier_def g0 notin pathstart_def) |
805 using `0 \<le> u` g0 disj |
805 using \<open>0 \<le> u\<close> g0 disj |
806 apply (simp add: path_image_subpath_gen) |
806 apply (simp add: path_image_subpath_gen) |
807 apply (auto simp: closed_segment_eq_real_ivl pathstart_def pathfinish_def subpath_def) |
807 apply (auto simp: closed_segment_eq_real_ivl pathstart_def pathfinish_def subpath_def) |
808 apply (rename_tac y) |
808 apply (rename_tac y) |
809 apply (drule_tac x="y/u" in spec) |
809 apply (drule_tac x="y/u" in spec) |
810 apply (auto split: split_if_asm) |
810 apply (auto split: split_if_asm) |
838 obtain h where h: "path h" "pathstart h = pathstart g" "path_image h \<subseteq> path_image g" |
838 obtain h where h: "path h" "pathstart h = pathstart g" "path_image h \<subseteq> path_image g" |
839 "path_image h - {pathfinish h} \<subseteq> interior S" |
839 "path_image h - {pathfinish h} \<subseteq> interior S" |
840 "pathfinish h \<in> frontier S" |
840 "pathfinish h \<in> frontier S" |
841 using exists_path_subpath_to_frontier [OF g _ g1] closure_closed [OF S] g0 by auto |
841 using exists_path_subpath_to_frontier [OF g _ g1] closure_closed [OF S] g0 by auto |
842 show ?thesis |
842 show ?thesis |
843 apply (rule that [OF `path h`]) |
843 apply (rule that [OF \<open>path h\<close>]) |
844 using assms h |
844 using assms h |
845 apply auto |
845 apply auto |
846 apply (metis diff_single_insert frontier_subset_eq insert_iff interior_subset subset_iff) |
846 apply (metis diff_single_insert frontier_subset_eq insert_iff interior_subset subset_iff) |
847 done |
847 done |
848 qed |
848 qed |
1553 using convex_imp_path_connected by auto |
1553 using convex_imp_path_connected by auto |
1554 next |
1554 next |
1555 case False |
1555 case False |
1556 then obtain a where "a \<in> s" by auto |
1556 then obtain a where "a \<in> s" by auto |
1557 { fix x y assume "x \<notin> s" "y \<notin> s" |
1557 { fix x y assume "x \<notin> s" "y \<notin> s" |
1558 then have "x \<noteq> a" "y \<noteq> a" using `a \<in> s` by auto |
1558 then have "x \<noteq> a" "y \<noteq> a" using \<open>a \<in> s\<close> by auto |
1559 then have bxy: "bounded(insert x (insert y s))" |
1559 then have bxy: "bounded(insert x (insert y s))" |
1560 by (simp add: `bounded s`) |
1560 by (simp add: \<open>bounded s\<close>) |
1561 then obtain B::real where B: "0 < B" and Bx: "norm (a - x) < B" and By: "norm (a - y) < B" |
1561 then obtain B::real where B: "0 < B" and Bx: "norm (a - x) < B" and By: "norm (a - y) < B" |
1562 and "s \<subseteq> ball a B" |
1562 and "s \<subseteq> ball a B" |
1563 using bounded_subset_ballD [OF bxy, of a] by (auto simp: dist_norm) |
1563 using bounded_subset_ballD [OF bxy, of a] by (auto simp: dist_norm) |
1564 def C == "B / norm(x - a)" |
1564 def C == "B / norm(x - a)" |
1565 { fix u |
1565 { fix u |
1566 assume u: "(1 - u) *\<^sub>R x + u *\<^sub>R (a + C *\<^sub>R (x - a)) \<in> s" and "0 \<le> u" "u \<le> 1" |
1566 assume u: "(1 - u) *\<^sub>R x + u *\<^sub>R (a + C *\<^sub>R (x - a)) \<in> s" and "0 \<le> u" "u \<le> 1" |
1567 have CC: "1 \<le> 1 + (C - 1) * u" |
1567 have CC: "1 \<le> 1 + (C - 1) * u" |
1568 using `x \<noteq> a` `0 \<le> u` |
1568 using \<open>x \<noteq> a\<close> \<open>0 \<le> u\<close> |
1569 apply (simp add: C_def divide_simps norm_minus_commute) |
1569 apply (simp add: C_def divide_simps norm_minus_commute) |
1570 using Bx by auto |
1570 using Bx by auto |
1571 have *: "\<And>v. (1 - u) *\<^sub>R x + u *\<^sub>R (a + v *\<^sub>R (x - a)) = a + (1 + (v - 1) * u) *\<^sub>R (x - a)" |
1571 have *: "\<And>v. (1 - u) *\<^sub>R x + u *\<^sub>R (a + v *\<^sub>R (x - a)) = a + (1 + (v - 1) * u) *\<^sub>R (x - a)" |
1572 by (simp add: algebra_simps) |
1572 by (simp add: algebra_simps) |
1573 have "a + ((1 / (1 + C * u - u)) *\<^sub>R x + ((u / (1 + C * u - u)) *\<^sub>R a + (C * u / (1 + C * u - u)) *\<^sub>R x)) = |
1573 have "a + ((1 / (1 + C * u - u)) *\<^sub>R x + ((u / (1 + C * u - u)) *\<^sub>R a + (C * u / (1 + C * u - u)) *\<^sub>R x)) = |
1581 ((u / (1 + C * u - u)) *\<^sub>R x + (C * u / (1 + C * u - u)) *\<^sub>R a))" |
1581 ((u / (1 + C * u - u)) *\<^sub>R x + (C * u / (1 + C * u - u)) *\<^sub>R a))" |
1582 using CC by (simp add: field_simps) (simp add: add_divide_distrib scaleR_add_left) |
1582 using CC by (simp add: field_simps) (simp add: add_divide_distrib scaleR_add_left) |
1583 finally have xeq: "(1 - 1 / (1 + (C - 1) * u)) *\<^sub>R a + (1 / (1 + (C - 1) * u)) *\<^sub>R (a + (1 + (C - 1) * u) *\<^sub>R (x - a)) = x" |
1583 finally have xeq: "(1 - 1 / (1 + (C - 1) * u)) *\<^sub>R a + (1 / (1 + (C - 1) * u)) *\<^sub>R (a + (1 + (C - 1) * u) *\<^sub>R (x - a)) = x" |
1584 by (simp add: algebra_simps) |
1584 by (simp add: algebra_simps) |
1585 have False |
1585 have False |
1586 using `convex s` |
1586 using \<open>convex s\<close> |
1587 apply (simp add: convex_alt) |
1587 apply (simp add: convex_alt) |
1588 apply (drule_tac x=a in bspec) |
1588 apply (drule_tac x=a in bspec) |
1589 apply (rule `a \<in> s`) |
1589 apply (rule \<open>a \<in> s\<close>) |
1590 apply (drule_tac x="a + (1 + (C - 1) * u) *\<^sub>R (x - a)" in bspec) |
1590 apply (drule_tac x="a + (1 + (C - 1) * u) *\<^sub>R (x - a)" in bspec) |
1591 using u apply (simp add: *) |
1591 using u apply (simp add: *) |
1592 apply (drule_tac x="1 / (1 + (C - 1) * u)" in spec) |
1592 apply (drule_tac x="1 / (1 + (C - 1) * u)" in spec) |
1593 using `x \<noteq> a` `x \<notin> s` `0 \<le> u` CC |
1593 using \<open>x \<noteq> a\<close> \<open>x \<notin> s\<close> \<open>0 \<le> u\<close> CC |
1594 apply (auto simp: xeq) |
1594 apply (auto simp: xeq) |
1595 done |
1595 done |
1596 } |
1596 } |
1597 then have pcx: "path_component (- s) x (a + C *\<^sub>R (x - a))" |
1597 then have pcx: "path_component (- s) x (a + C *\<^sub>R (x - a))" |
1598 by (force simp: closed_segment_def intro!: path_connected_linepath) |
1598 by (force simp: closed_segment_def intro!: path_connected_linepath) |
1599 def D == "B / norm(y - a)" --{*massive duplication with the proof above*} |
1599 def D == "B / norm(y - a)" \<comment>\<open>massive duplication with the proof above\<close> |
1600 { fix u |
1600 { fix u |
1601 assume u: "(1 - u) *\<^sub>R y + u *\<^sub>R (a + D *\<^sub>R (y - a)) \<in> s" and "0 \<le> u" "u \<le> 1" |
1601 assume u: "(1 - u) *\<^sub>R y + u *\<^sub>R (a + D *\<^sub>R (y - a)) \<in> s" and "0 \<le> u" "u \<le> 1" |
1602 have DD: "1 \<le> 1 + (D - 1) * u" |
1602 have DD: "1 \<le> 1 + (D - 1) * u" |
1603 using `y \<noteq> a` `0 \<le> u` |
1603 using \<open>y \<noteq> a\<close> \<open>0 \<le> u\<close> |
1604 apply (simp add: D_def divide_simps norm_minus_commute) |
1604 apply (simp add: D_def divide_simps norm_minus_commute) |
1605 using By by auto |
1605 using By by auto |
1606 have *: "\<And>v. (1 - u) *\<^sub>R y + u *\<^sub>R (a + v *\<^sub>R (y - a)) = a + (1 + (v - 1) * u) *\<^sub>R (y - a)" |
1606 have *: "\<And>v. (1 - u) *\<^sub>R y + u *\<^sub>R (a + v *\<^sub>R (y - a)) = a + (1 + (v - 1) * u) *\<^sub>R (y - a)" |
1607 by (simp add: algebra_simps) |
1607 by (simp add: algebra_simps) |
1608 have "a + ((1 / (1 + D * u - u)) *\<^sub>R y + ((u / (1 + D * u - u)) *\<^sub>R a + (D * u / (1 + D * u - u)) *\<^sub>R y)) = |
1608 have "a + ((1 / (1 + D * u - u)) *\<^sub>R y + ((u / (1 + D * u - u)) *\<^sub>R a + (D * u / (1 + D * u - u)) *\<^sub>R y)) = |
1616 ((u / (1 + D * u - u)) *\<^sub>R y + (D * u / (1 + D * u - u)) *\<^sub>R a))" |
1616 ((u / (1 + D * u - u)) *\<^sub>R y + (D * u / (1 + D * u - u)) *\<^sub>R a))" |
1617 using DD by (simp add: field_simps) (simp add: add_divide_distrib scaleR_add_left) |
1617 using DD by (simp add: field_simps) (simp add: add_divide_distrib scaleR_add_left) |
1618 finally have xeq: "(1 - 1 / (1 + (D - 1) * u)) *\<^sub>R a + (1 / (1 + (D - 1) * u)) *\<^sub>R (a + (1 + (D - 1) * u) *\<^sub>R (y - a)) = y" |
1618 finally have xeq: "(1 - 1 / (1 + (D - 1) * u)) *\<^sub>R a + (1 / (1 + (D - 1) * u)) *\<^sub>R (a + (1 + (D - 1) * u) *\<^sub>R (y - a)) = y" |
1619 by (simp add: algebra_simps) |
1619 by (simp add: algebra_simps) |
1620 have False |
1620 have False |
1621 using `convex s` |
1621 using \<open>convex s\<close> |
1622 apply (simp add: convex_alt) |
1622 apply (simp add: convex_alt) |
1623 apply (drule_tac x=a in bspec) |
1623 apply (drule_tac x=a in bspec) |
1624 apply (rule `a \<in> s`) |
1624 apply (rule \<open>a \<in> s\<close>) |
1625 apply (drule_tac x="a + (1 + (D - 1) * u) *\<^sub>R (y - a)" in bspec) |
1625 apply (drule_tac x="a + (1 + (D - 1) * u) *\<^sub>R (y - a)" in bspec) |
1626 using u apply (simp add: *) |
1626 using u apply (simp add: *) |
1627 apply (drule_tac x="1 / (1 + (D - 1) * u)" in spec) |
1627 apply (drule_tac x="1 / (1 + (D - 1) * u)" in spec) |
1628 using `y \<noteq> a` `y \<notin> s` `0 \<le> u` DD |
1628 using \<open>y \<noteq> a\<close> \<open>y \<notin> s\<close> \<open>0 \<le> u\<close> DD |
1629 apply (auto simp: xeq) |
1629 apply (auto simp: xeq) |
1630 done |
1630 done |
1631 } |
1631 } |
1632 then have pdy: "path_component (- s) y (a + D *\<^sub>R (y - a))" |
1632 then have pdy: "path_component (- s) y (a + D *\<^sub>R (y - a))" |
1633 by (force simp: closed_segment_def intro!: path_connected_linepath) |
1633 by (force simp: closed_segment_def intro!: path_connected_linepath) |
1634 have pyx: "path_component (- s) (a + D *\<^sub>R (y - a)) (a + C *\<^sub>R (x - a))" |
1634 have pyx: "path_component (- s) (a + D *\<^sub>R (y - a)) (a + C *\<^sub>R (x - a))" |
1635 apply (rule path_component_of_subset [of "{x. norm(x - a) = B}"]) |
1635 apply (rule path_component_of_subset [of "{x. norm(x - a) = B}"]) |
1636 using `s \<subseteq> ball a B` |
1636 using \<open>s \<subseteq> ball a B\<close> |
1637 apply (force simp: ball_def dist_norm norm_minus_commute) |
1637 apply (force simp: ball_def dist_norm norm_minus_commute) |
1638 apply (rule path_connected_sphere [OF 2, of a B, simplified path_connected_component, rule_format]) |
1638 apply (rule path_connected_sphere [OF 2, of a B, simplified path_connected_component, rule_format]) |
1639 using `x \<noteq> a` using `y \<noteq> a` B apply (auto simp: C_def D_def) |
1639 using \<open>x \<noteq> a\<close> using \<open>y \<noteq> a\<close> B apply (auto simp: C_def D_def) |
1640 done |
1640 done |
1641 have "path_component (- s) x y" |
1641 have "path_component (- s) x y" |
1642 by (metis path_component_trans path_component_sym pcx pdy pyx) |
1642 by (metis path_component_trans path_component_sym pcx pdy pyx) |
1643 } |
1643 } |
1644 then show ?thesis |
1644 then show ?thesis |
1832 assumes "x \<ge> B" "y \<ge> B" "0 \<le> u" "u \<le> 1" |
1832 assumes "x \<ge> B" "y \<ge> B" "0 \<le> u" "u \<le> 1" |
1833 shows "(1 - u) * x + u * y \<ge> B" |
1833 shows "(1 - u) * x + u * y \<ge> B" |
1834 proof - |
1834 proof - |
1835 obtain dx dy where "dx \<ge> 0" "dy \<ge> 0" "x = B + dx" "y = B + dy" |
1835 obtain dx dy where "dx \<ge> 0" "dy \<ge> 0" "x = B + dx" "y = B + dy" |
1836 using assms by auto (metis add.commute diff_add_cancel) |
1836 using assms by auto (metis add.commute diff_add_cancel) |
1837 with `0 \<le> u` `u \<le> 1` show ?thesis |
1837 with \<open>0 \<le> u\<close> \<open>u \<le> 1\<close> show ?thesis |
1838 by (simp add: add_increasing2 mult_left_le field_simps) |
1838 by (simp add: add_increasing2 mult_left_le field_simps) |
1839 qed |
1839 qed |
1840 |
1840 |
1841 lemma cobounded_outside: |
1841 lemma cobounded_outside: |
1842 fixes s :: "'a :: real_normed_vector set" |
1842 fixes s :: "'a :: real_normed_vector set" |
2034 { assume "bounded (connected_component_set (- s) z)" |
2034 { assume "bounded (connected_component_set (- s) z)" |
2035 with bounded_pos_less obtain B where "B>0" and B: "\<And>x. connected_component (- s) z x \<Longrightarrow> norm x < B" |
2035 with bounded_pos_less obtain B where "B>0" and B: "\<And>x. connected_component (- s) z x \<Longrightarrow> norm x < B" |
2036 by (metis mem_Collect_eq) |
2036 by (metis mem_Collect_eq) |
2037 def C \<equiv> "((B + 1 + norm z) / norm (z-a))" |
2037 def C \<equiv> "((B + 1 + norm z) / norm (z-a))" |
2038 have "C > 0" |
2038 have "C > 0" |
2039 using `0 < B` zna by (simp add: C_def divide_simps add_strict_increasing) |
2039 using \<open>0 < B\<close> zna by (simp add: C_def divide_simps add_strict_increasing) |
2040 have "\<bar>norm (z + C *\<^sub>R (z-a)) - norm (C *\<^sub>R (z-a))\<bar> \<le> norm z" |
2040 have "\<bar>norm (z + C *\<^sub>R (z-a)) - norm (C *\<^sub>R (z-a))\<bar> \<le> norm z" |
2041 by (metis add_diff_cancel norm_triangle_ineq3) |
2041 by (metis add_diff_cancel norm_triangle_ineq3) |
2042 moreover have "norm (C *\<^sub>R (z-a)) > norm z + B" |
2042 moreover have "norm (C *\<^sub>R (z-a)) > norm z + B" |
2043 using zna `B>0` by (simp add: C_def le_max_iff_disj field_simps) |
2043 using zna \<open>B>0\<close> by (simp add: C_def le_max_iff_disj field_simps) |
2044 ultimately have C: "norm (z + C *\<^sub>R (z-a)) > B" by linarith |
2044 ultimately have C: "norm (z + C *\<^sub>R (z-a)) > B" by linarith |
2045 { fix u::real |
2045 { fix u::real |
2046 assume u: "0\<le>u" "u\<le>1" and ins: "(1 - u) *\<^sub>R z + u *\<^sub>R (z + C *\<^sub>R (z - a)) \<in> s" |
2046 assume u: "0\<le>u" "u\<le>1" and ins: "(1 - u) *\<^sub>R z + u *\<^sub>R (z + C *\<^sub>R (z - a)) \<in> s" |
2047 then have Cpos: "1 + u * C > 0" |
2047 then have Cpos: "1 + u * C > 0" |
2048 by (meson `0 < C` add_pos_nonneg less_eq_real_def zero_le_mult_iff zero_less_one) |
2048 by (meson \<open>0 < C\<close> add_pos_nonneg less_eq_real_def zero_le_mult_iff zero_less_one) |
2049 then have *: "(1 / (1 + u * C)) *\<^sub>R z + (u * C / (1 + u * C)) *\<^sub>R z = z" |
2049 then have *: "(1 / (1 + u * C)) *\<^sub>R z + (u * C / (1 + u * C)) *\<^sub>R z = z" |
2050 by (simp add: scaleR_add_left [symmetric] divide_simps) |
2050 by (simp add: scaleR_add_left [symmetric] divide_simps) |
2051 then have False |
2051 then have False |
2052 using convexD_alt [OF s `a \<in> s` ins, of "1/(u*C + 1)"] `C>0` `z \<notin> s` Cpos u |
2052 using convexD_alt [OF s \<open>a \<in> s\<close> ins, of "1/(u*C + 1)"] \<open>C>0\<close> \<open>z \<notin> s\<close> Cpos u |
2053 by (simp add: * divide_simps algebra_simps) |
2053 by (simp add: * divide_simps algebra_simps) |
2054 } note contra = this |
2054 } note contra = this |
2055 have "connected_component (- s) z (z + C *\<^sub>R (z-a))" |
2055 have "connected_component (- s) z (z + C *\<^sub>R (z-a))" |
2056 apply (rule connected_componentI [OF connected_segment [of z "z + C *\<^sub>R (z-a)"]]) |
2056 apply (rule connected_componentI [OF connected_segment [of z "z + C *\<^sub>R (z-a)"]]) |
2057 apply (simp add: closed_segment_def) |
2057 apply (simp add: closed_segment_def) |
2248 proof (cases "a \<in> t") |
2248 proof (cases "a \<in> t") |
2249 case True with a show ?thesis by blast |
2249 case True with a show ?thesis by blast |
2250 next |
2250 next |
2251 case False |
2251 case False |
2252 have front: "frontier t \<subseteq> - s" |
2252 have front: "frontier t \<subseteq> - s" |
2253 using `s \<subseteq> t` frontier_disjoint_eq t by auto |
2253 using \<open>s \<subseteq> t\<close> frontier_disjoint_eq t by auto |
2254 { fix \<gamma> |
2254 { fix \<gamma> |
2255 assume "path \<gamma>" and pimg_sbs: "path_image \<gamma> - {pathfinish \<gamma>} \<subseteq> interior (- t)" |
2255 assume "path \<gamma>" and pimg_sbs: "path_image \<gamma> - {pathfinish \<gamma>} \<subseteq> interior (- t)" |
2256 and pf: "pathfinish \<gamma> \<in> frontier t" and ps: "pathstart \<gamma> = a" |
2256 and pf: "pathfinish \<gamma> \<in> frontier t" and ps: "pathstart \<gamma> = a" |
2257 def c \<equiv> "pathfinish \<gamma>" |
2257 def c \<equiv> "pathfinish \<gamma>" |
2258 have "c \<in> -s" unfolding c_def using front pf by blast |
2258 have "c \<in> -s" unfolding c_def using front pf by blast |
2265 then have "d \<in> -s" using \<epsilon> |
2265 then have "d \<in> -s" using \<epsilon> |
2266 using dist_commute by (metis contra_subsetD mem_cball not_le not_less_iff_gr_or_eq) |
2266 using dist_commute by (metis contra_subsetD mem_cball not_le not_less_iff_gr_or_eq) |
2267 have pimg_sbs_cos: "path_image \<gamma> \<subseteq> -s" |
2267 have pimg_sbs_cos: "path_image \<gamma> \<subseteq> -s" |
2268 using pimg_sbs apply (auto simp: path_image_def) |
2268 using pimg_sbs apply (auto simp: path_image_def) |
2269 apply (drule subsetD) |
2269 apply (drule subsetD) |
2270 using `c \<in> - s` `s \<subseteq> t` interior_subset apply (auto simp: c_def) |
2270 using \<open>c \<in> - s\<close> \<open>s \<subseteq> t\<close> interior_subset apply (auto simp: c_def) |
2271 done |
2271 done |
2272 have "closed_segment c d \<le> cball c \<epsilon>" |
2272 have "closed_segment c d \<le> cball c \<epsilon>" |
2273 apply (simp add: segment_convex_hull) |
2273 apply (simp add: segment_convex_hull) |
2274 apply (rule hull_minimal) |
2274 apply (rule hull_minimal) |
2275 using `\<epsilon> > 0` d apply (auto simp: dist_commute) |
2275 using \<open>\<epsilon> > 0\<close> d apply (auto simp: dist_commute) |
2276 done |
2276 done |
2277 with \<epsilon> have "closed_segment c d \<subseteq> -s" by blast |
2277 with \<epsilon> have "closed_segment c d \<subseteq> -s" by blast |
2278 moreover have con_gcd: "connected (path_image \<gamma> \<union> closed_segment c d)" |
2278 moreover have con_gcd: "connected (path_image \<gamma> \<union> closed_segment c d)" |
2279 by (rule connected_Un) (auto simp: c_def `path \<gamma>` connected_path_image) |
2279 by (rule connected_Un) (auto simp: c_def \<open>path \<gamma>\<close> connected_path_image) |
2280 ultimately have "connected_component (- s) a d" |
2280 ultimately have "connected_component (- s) a d" |
2281 unfolding connected_component_def using pimg_sbs_cos ps by blast |
2281 unfolding connected_component_def using pimg_sbs_cos ps by blast |
2282 then have "outside s \<inter> t \<noteq> {}" |
2282 then have "outside s \<inter> t \<noteq> {}" |
2283 using outside_same_component [OF _ a] by (metis IntI `d \<in> t` empty_iff) |
2283 using outside_same_component [OF _ a] by (metis IntI \<open>d \<in> t\<close> empty_iff) |
2284 } note * = this |
2284 } note * = this |
2285 have pal: "pathstart (linepath a b) \<in> closure (- t)" |
2285 have pal: "pathstart (linepath a b) \<in> closure (- t)" |
2286 by (auto simp: False closure_def) |
2286 by (auto simp: False closure_def) |
2287 show ?thesis |
2287 show ?thesis |
2288 by (rule exists_path_subpath_to_frontier [OF path_linepath pal _ *]) (auto simp: b) |
2288 by (rule exists_path_subpath_to_frontier [OF path_linepath pal _ *]) (auto simp: b) |
2326 have "s \<inter> t = {}" using assms |
2326 have "s \<inter> t = {}" using assms |
2327 by (metis disjoint_iff_not_equal inside_no_overlap subsetCE) |
2327 by (metis disjoint_iff_not_equal inside_no_overlap subsetCE) |
2328 moreover have "outside s \<inter> inside t \<noteq> {}" |
2328 moreover have "outside s \<inter> inside t \<noteq> {}" |
2329 by (meson False assms(4) compact_eq_bounded_closed coms open_inside outside_compact_in_open t) |
2329 by (meson False assms(4) compact_eq_bounded_closed coms open_inside outside_compact_in_open t) |
2330 ultimately have "inside s \<inter> t = {}" |
2330 ultimately have "inside s \<inter> t = {}" |
2331 using inside_outside_intersect_connected [OF `connected t`, of s] |
2331 using inside_outside_intersect_connected [OF \<open>connected t\<close>, of s] |
2332 by (metis "2" compact_eq_bounded_closed coms connected_outside inf.commute inside_outside_intersect_connected outst) |
2332 by (metis "2" compact_eq_bounded_closed coms connected_outside inf.commute inside_outside_intersect_connected outst) |
2333 then show ?thesis |
2333 then show ?thesis |
2334 using inside_inside [OF `s \<subseteq> inside t`] by blast |
2334 using inside_inside [OF \<open>s \<subseteq> inside t\<close>] by blast |
2335 qed |
2335 qed |
2336 qed |
2336 qed |
2337 |
2337 |
2338 lemma connected_with_inside: |
2338 lemma connected_with_inside: |
2339 fixes s :: "'a :: real_normed_vector set" |
2339 fixes s :: "'a :: real_normed_vector set" |