---

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


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. t : ℚ
9. (t * qdot(v;p)) ≤ (t * r)
10. dimension(qv-add(qv-mul(t;p);qv-mul(1 - t;q))) = dimension(v) ∈ ℤ
11. 0 ≤ t
12. t ≤ 1
13. ((1 - t) * qdot(v;q)) ≤ ((1 - t) * r)
⊢ ((t * qdot(v;p)) + ((1 - t) * qdot(v;q))) ≤ r
BY
{ (RWO "-1 -5" 0 THENA Auto) }

1
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. t : ℚ
9. (t * qdot(v;p)) ≤ (t * r)
10. dimension(qv-add(qv-mul(t;p);qv-mul(1 - t;q))) = dimension(v) ∈ ℤ
11. 0 ≤ t
12. t ≤ 1
13. ((1 - t) * qdot(v;q)) ≤ ((1 - t) * r)
⊢ ((t * r) + ((1 - t) * r)) ≤ r

---

Latex:

---

Latex:

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.  t  :  \mBbbQ{}
9.  (t  *  qdot(v;p))  \mleq{}  (t  *  r)
10.  dimension(qv-add(qv-mul(t;p);qv-mul(1  -  t;q)))  =  dimension(v)
11.  0  \mleq{}  t
12.  t  \mleq{}  1
13.  ((1  -  t)  *  qdot(v;q))  \mleq{}  ((1  -  t)  *  r)
\mvdash{}  ((t  *  qdot(v;p))  +  ((1  -  t)  *  qdot(v;q)))  \mleq{}  r


By

---

Latex:
(RWO  "-1  -5"  0  THENA  Auto)

---

Home Index