---

Step * of Lemma convex-comb-same

∀[x,r:ℝ]. ∀[s:{s:ℝ| r + s ≠ r0} ].  (convex-comb(x;x;r;s) = x)
BY
{ (Intros THEN (RWO "convex-comb-req" 0 THENA Auto) THEN DVar `s' THEN Unhide THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Intros  THEN  (RWO  "convex-comb-req"  0  THENA  Auto)  THEN  DVar  `s'  THEN  Unhide  THEN  Auto)

---

Home Index