---

Step * of Lemma convex-comb-rless2

∀x:ℝ. ∀y:{y:ℝ| x < y} . ∀r:{r:ℝ| r0 < r} . ∀s:{s:ℝ| r0 < (r + s)} . ∀t:{t:ℝ| s < t} .
  (convex-comb(x;y;r;s) < convex-comb(x;y;r;t))
BY
{ (Auto
   THEN DVar `s'
   THEN (Assert r + t ≠ r0 BY
               (DVar `t' THEN Unhide THEN Auto THEN nRAdd ⌜r⌝ (-1)⋅ THEN Auto))
   THEN Unfold `convex-comb` 0
   THEN BLemma `fractions-rless`
   THEN Auto) }

1
1. x : ℝ
2. y : {y:ℝ| x < y} 
3. r : {r:ℝ| r0 < r} 
4. s : ℝ
5. [%1] : r0 < (r + s)
6. t : {t:ℝ| s < t} 
7. r + t ≠ r0
⊢ r0 < (r + t)

2
1. x : ℝ
2. y : {y:ℝ| x < y} 
3. r : {r:ℝ| r0 < r} 
4. s : ℝ
5. [%1] : r0 < (r + s)
6. t : {t:ℝ| s < t} 
7. r + t ≠ r0
⊢ (((r * x) + (s * y)) * (r + t)) < (((r * x) + (t * y)) * (r + s))

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  \mforall{}y:\{y:\mBbbR{}|  x  <  y\}  .  \mforall{}r:\{r:\mBbbR{}|  r0  <  r\}  .  \mforall{}s:\{s:\mBbbR{}|  r0  <  (r  +  s)\}  .  \mforall{}t:\{t:\mBbbR{}|  s  <  t\}  .
    (convex-comb(x;y;r;s)  <  convex-comb(x;y;r;t))


By

---

Latex:
(Auto
  THEN  DVar  `s'
  THEN  (Assert  r  +  t  \mneq{}  r0  BY
                          (DVar  `t'  THEN  Unhide  THEN  Auto  THEN  nRAdd  \mkleeneopen{}r\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto))
  THEN  Unfold  `convex-comb`  0
  THEN  BLemma  `fractions-rless`
  THEN  Auto)

---

Home Index