---

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

1
.....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. r ≤ qdot(v;q)
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 * r) ≤ (t * qdot(v;p))
⊢ 0 ≤ (1 - t)

2
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)))

---

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


By

---

Latex:
((QMul  \mkleeneopen{}t\mkleeneclose{}  7\mcdot{}  THENA  Auto)  THEN  (QMul  \mkleeneopen{}1  -  t\mkleeneclose{}  8\mcdot{}  THENA  Auto))

---

Home Index