---

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

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 * 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

---

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.  qdot(v;p)  \mleq{}  r
8.  dimension(q)  =  dimension(v)
9.  qdot(v;q)  \mleq{}  r
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{}  ((t  *  qdot(v;p))  +  ((1  -  t)  *  qdot(v;q)))  \mleq{}  r


By

---

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

---

Home Index