---

Step * of Lemma convex-comb-strict-upper-bound

∀r,s:{s:ℝ| r0 < s} . ∀x,y:ℝ.  ((x < y) ⇒ (convex-comb(x;y;r;s) < y))
BY
{ ((Auto THEN Unfold `convex-comb` 0)
   THEN (Assert r0 < (r + s) BY
               (DSetVars THEN (Unhide THEN Auto) THEN RWO "2<" 0 THEN Auto))
   THEN (nRMul ⌜r + s⌝ 0⋅ THENA Auto)) }

1
1. r : {r:ℝ| r0 < r} 
2. s : {s:ℝ| r0 < s} 
3. x : ℝ
4. y : ℝ
5. x < y
6. r0 < (r + s)
⊢ ((r * x) + (s * y)) < ((r * y) + (s * y))

---

Latex:

---

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


By

---

Latex:
((Auto  THEN  Unfold  `convex-comb`  0)
  THEN  (Assert  r0  <  (r  +  s)  BY
                          (DSetVars  THEN  (Unhide  THEN  Auto)  THEN  RWO  "2<"  0  THEN  Auto))
  THEN  (nRMul  \mkleeneopen{}r  +  s\mkleeneclose{}  0\mcdot{}  THENA  Auto))

---

Home Index