---

Step * of Lemma std-simplex-properties

∀[n:ℕ]. ∀[v:Δ(n)].  ((∀i:ℕn + 1. (r0 ≤ (v i))) ∧ (Σ{v i | 0≤i≤n} = r1))
BY
{ (Auto THEN DVar `v' THEN Unhide THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[v:\mDelta{}(n)].    ((\mforall{}i:\mBbbN{}n  +  1.  (r0  \mleq{}  (v  i)))  \mwedge{}  (\mSigma{}\{v  i  |  0\mleq{}i\mleq{}n\}  =  r1))


By

---

Latex:
(Auto  THEN  DVar  `v'  THEN  Unhide  THEN  Auto)

---

Home Index