---

Step * 1 2 of Lemma qv-convex-upper-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 * r) ≤ (t * qdot(v;p))
10. dimension(qv-add(qv-mul(t;p);qv-mul(1 - t;q))) = dimension(v) ∈ ℤ
11. 0 ≤ t
12. t ≤ 1
13. ((1 - t) * r) ≤ ((1 - t) * qdot(v;q))
⊢ r ≤ ((t * qdot(v;p)) + ((1 - t) * qdot(v;q)))
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 * r) ≤ (t * qdot(v;p))
10. dimension(qv-add(qv-mul(t;p);qv-mul(1 - t;q))) = dimension(v) ∈ ℤ
11. 0 ≤ t
12. t ≤ 1
13. ((1 - t) * r) ≤ ((1 - t) * qdot(v;q))
⊢ r ≤ ((t * r) + ((1 - t) * 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  *  r)  \mleq{}  (t  *  qdot(v;p))
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)  *  r)  \mleq{}  ((1  -  t)  *  qdot(v;q))
\mvdash{}  r  \mleq{}  ((t  *  qdot(v;p))  +  ((1  -  t)  *  qdot(v;q)))


By

---

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

---

Home Index