---

Step * of Lemma qv-convex_wf

∀[S:(ℚ List) ⟶ ℙ]. (qv-convex(p.S[p]) ∈ ℙ)
BY
{ xxx(ProveWfLemma THEN RWO "dim-qv-mul" 0 THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[S:(\mBbbQ{}  List)  {}\mrightarrow{}  \mBbbP{}].  (qv-convex(p.S[p])  \mmember{}  \mBbbP{})


By

---

Latex:
xxx(ProveWfLemma  THEN  RWO  "dim-qv-mul"  0  THEN  Auto)xxx

---

Home Index