---

Step * of Lemma std-simplex-void

∀[n:ℤ]. ¬Δ(n) supposing n < 0
BY
{ (Auto THEN (D 0 THENA Auto) THEN RepeatFor 2 (D -1)) }

1
1. n : ℤ
2. n < 0
3. v : ℝ^n + 1
4. ∀i:ℕn + 1. (r0 ≤ (v i))
5. Σ{v i | 0≤i≤n} = r1
⊢ False

---

Latex:

---

Latex:
\mforall{}[n:\mBbbZ{}].  \mneg{}\mDelta{}(n)  supposing  n  <  0


By

---

Latex:
(Auto  THEN  (D  0  THENA  Auto)  THEN  RepeatFor  2  (D  -1))

---

Home Index