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