equal
deleted
inserted
replaced
271 txt{* Now we show |
271 txt{* Now we show |
272 $h\ap y + a \cdot \xi\leq p\ap (y\plus a \mult x_0)$ |
272 $h\ap y + a \cdot \xi\leq p\ap (y\plus a \mult x_0)$ |
273 by case analysis on $a$. *}; |
273 by case analysis on $a$. *}; |
274 |
274 |
275 also; have "... <= p (y + a \<cdot> x0)"; |
275 also; have "... <= p (y + a \<cdot> x0)"; |
276 proof (rule linorder_less_split); |
276 proof (rule linorder_cases); |
277 |
277 |
278 assume z: "a = #0"; |
278 assume z: "a = #0"; |
279 with vs y a; show ?thesis; by simp; |
279 with vs y a; show ?thesis; by simp; |
280 |
280 |
281 txt {* In the case $a < 0$, we use $a_1$ with $\idt{ya}$ |
281 txt {* In the case $a < 0$, we use $a_1$ with $\idt{ya}$ |