---

Step * of Lemma convex-comb-req

∀[x,y,r:ℝ]. ∀[s:{s:ℝ| r + s ≠ r0} ].  (convex-comb(x;y;r;s) = (((r1 - (s/r + s)) * x) + ((s/r + s) * y)))
BY
{ (Intros THEN RepUR ``convex-comb`` 0 THEN nRMul ⌜r + s⌝ 0⋅ THEN Auto THEN DVar `s' THEN Unhide THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x,y,r:\mBbbR{}].  \mforall{}[s:\{s:\mBbbR{}|  r  +  s  \mneq{}  r0\}  ].
    (convex-comb(x;y;r;s)  =  (((r1  -  (s/r  +  s))  *  x)  +  ((s/r  +  s)  *  y)))


By

---

Latex:
(Intros
  THEN  RepUR  ``convex-comb``  0
  THEN  nRMul  \mkleeneopen{}r  +  s\mkleeneclose{}  0\mcdot{}
  THEN  Auto
  THEN  DVar  `s'
  THEN  Unhide
  THEN  Auto)

---

Home Index