equal
deleted
inserted
replaced
1260 then have "x *\<^sub>R (a - b) = y *\<^sub>R (a - b)" |
1260 then have "x *\<^sub>R (a - b) = y *\<^sub>R (a - b)" |
1261 by (auto simp: algebra_simps) |
1261 by (auto simp: algebra_simps) |
1262 then show "x=y" |
1262 then show "x=y" |
1263 using assms by auto |
1263 using assms by auto |
1264 qed |
1264 qed |
|
1265 |
|
1266 lemma linepath_le_1: |
|
1267 fixes a::"'a::linordered_idom" shows "\<lbrakk>a \<le> 1; b \<le> 1; 0 \<le> u; u \<le> 1\<rbrakk> \<Longrightarrow> (1 - u) * a + u * b \<le> 1" |
|
1268 using mult_left_le [of a "1-u"] mult_left_le [of b u] by auto |
1265 |
1269 |
1266 |
1270 |
1267 subsection%unimportant\<open>Segments via convex hulls\<close> |
1271 subsection%unimportant\<open>Segments via convex hulls\<close> |
1268 |
1272 |
1269 lemma segments_subset_convex_hull: |
1273 lemma segments_subset_convex_hull: |