---

Step * of Lemma convex-comb_wf

∀[I:Interval]. ∀[x,y:{x:ℝ| x ∈ I} ]. ∀[r:{r:ℝ| r0 ≤ r} ]. ∀[s:{s:ℝ| (r0 ≤ s) ∧ (r0 < (r + s))} ].
  (convex-comb(x;y;r;s) ∈ {x:ℝ| x ∈ I} )
BY
{ (Auto THEN DSetVars THEN MemTypeCD THEN Auto THEN ProveWfLemma) }

1
1. I : Interval
2. x : ℝ
3. x ∈ I
4. y : ℝ
5. y ∈ I
6. r : ℝ
7. r0 ≤ r
8. s : ℝ
9. r0 ≤ s
10. r0 < (r + s)
⊢ ((r * x) + (s * y)/r + s) ∈ I

---

Latex:

---

Latex:
\mforall{}[I:Interval].  \mforall{}[x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  ].  \mforall{}[r:\{r:\mBbbR{}|  r0  \mleq{}  r\}  ].  \mforall{}[s:\{s:\mBbbR{}|  (r0  \mleq{}  s)  \mwedge{}  (r0  <  (r  +  s))\}  ].
    (convex-comb(x;y;r;s)  \mmember{}  \{x:\mBbbR{}|  x  \mmember{}  I\}  )


By

---

Latex:
(Auto  THEN  DSetVars  THEN  MemTypeCD  THEN  Auto  THEN  ProveWfLemma)

---

Home Index