---

Step * 1 1 of Lemma qv-convex-lower-half

.....antecedent..... 
1. r : ℚ
2. v : ℚ List
3. p : ℚ List
4. q : ℚ List
5. dimension(p) = dimension(q) ∈ ℤ
6. dimension(p) = dimension(v) ∈ ℤ
7. dimension(q) = dimension(v) ∈ ℤ
8. qdot(v;q) ≤ r
9. t : ℚ
10. dimension(qv-add(qv-mul(t;p);qv-mul(1 - t;q))) = dimension(v) ∈ ℤ
11. 0 ≤ t
12. t ≤ 1
13. (t * qdot(v;p)) ≤ (t * r)
⊢ 0 ≤ (1 - t)
BY
{ (QAdd ⌜t⌝ 0⋅ THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  r  :  \mBbbQ{}
2.  v  :  \mBbbQ{}  List
3.  p  :  \mBbbQ{}  List
4.  q  :  \mBbbQ{}  List
5.  dimension(p)  =  dimension(q)
6.  dimension(p)  =  dimension(v)
7.  dimension(q)  =  dimension(v)
8.  qdot(v;q)  \mleq{}  r
9.  t  :  \mBbbQ{}
10.  dimension(qv-add(qv-mul(t;p);qv-mul(1  -  t;q)))  =  dimension(v)
11.  0  \mleq{}  t
12.  t  \mleq{}  1
13.  (t  *  qdot(v;p))  \mleq{}  (t  *  r)
\mvdash{}  0  \mleq{}  (1  -  t)


By

---

Latex:
(QAdd  \mkleeneopen{}t\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index