---

Step * of Lemma qv-convex-lower-half

No Annotations
∀[r:ℚ]. ∀[v:ℚ List].  qv-convex(p.(dimension(p) = dimension(v) ∈ ℤ) ∧ (qdot(v;p) ≤ r))
BY
{ (Auto
   THEN All (Unfold `qv-convex`)
   THEN Auto
   THEN Repeat ((RWO "qdot-linear qdot-linear2 dim-qv-add dim-qv-mul" 0 THEN Auto))) }

1
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

---

Latex:

---

Latex:
No  Annotations
\mforall{}[r:\mBbbQ{}].  \mforall{}[v:\mBbbQ{}  List].    qv-convex(p.(dimension(p)  =  dimension(v))  \mwedge{}  (qdot(v;p)  \mleq{}  r))


By

---

Latex:
(Auto
  THEN  All  (Unfold  `qv-convex`)
  THEN  Auto
  THEN  Repeat  ((RWO  "qdot-linear  qdot-linear2  dim-qv-add  dim-qv-mul"  0  THEN  Auto)))

---

Home Index