equal
deleted
inserted
replaced
1875 fix y assume "dist (u *\<^sub>R x) y < 1 - u" |
1875 fix y assume "dist (u *\<^sub>R x) y < 1 - u" |
1876 hence "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> s" |
1876 hence "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> s" |
1877 using assms(3) apply(erule_tac subsetD) unfolding mem_cball dist_commute dist_norm |
1877 using assms(3) apply(erule_tac subsetD) unfolding mem_cball dist_commute dist_norm |
1878 unfolding group_add_class.diff_0 group_add_class.diff_0_right norm_minus_cancel norm_scaleR |
1878 unfolding group_add_class.diff_0 group_add_class.diff_0_right norm_minus_cancel norm_scaleR |
1879 apply (rule mult_left_le_imp_le[of "1 - u"]) |
1879 apply (rule mult_left_le_imp_le[of "1 - u"]) |
1880 unfolding normalizing.mul_a using `u<1` by auto |
1880 unfolding mult_assoc[symmetric] using `u<1` by auto |
1881 thus "y \<in> s" using assms(1)[unfolded convex_def, rule_format, of "inverse(1 - u) *\<^sub>R (y - u *\<^sub>R x)" x "1 - u" u] |
1881 thus "y \<in> s" using assms(1)[unfolded convex_def, rule_format, of "inverse(1 - u) *\<^sub>R (y - u *\<^sub>R x)" x "1 - u" u] |
1882 using as unfolding scaleR_scaleR by auto qed auto |
1882 using as unfolding scaleR_scaleR by auto qed auto |
1883 thus "u *\<^sub>R x \<in> s - frontier s" using frontier_def and interior_subset by auto qed |
1883 thus "u *\<^sub>R x \<in> s - frontier s" using frontier_def and interior_subset by auto qed |
1884 |
1884 |
1885 lemma homeomorphic_convex_compact_cball: fixes e::real and s::"(real^'n) set" |
1885 lemma homeomorphic_convex_compact_cball: fixes e::real and s::"(real^'n) set" |