---

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

∀r,s:{s:ℝ| r0 < s} . ∀x,y:ℝ.  ((y < x) ⇒ (convex-comb(x;y;r;s) < x))
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. y < x
6. r0 < (r + s)
⊢ ((r * x) + (s * y)) < ((r * x) + (s * x))

---

Latex:

---

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


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