---

Step * 1 of Lemma simplex-face_wf


1. n : ℤ
2. v : Δ(n)
3. i : ℕn + 2
4. 0 ≤ n
5. ∀i:ℕn + 1. (r0 ≤ (v i))
6. Σ{v i | 0≤i≤n} = r1
7. ∀i@0:ℕ(n + 1) + 1. (r0 ≤ if i@0 <z i then v i@0 if i <z i@0 then v (i@0 - 1) else r0 fi )
⊢ Σ{if i@0 <z i then v i@0 if i <z i@0 then v (i@0 - 1) else r0 fi  | 0≤i@0≤n + 1} = r1
BY
{ PromoteHyp 4 2 }

1
1. n : ℤ
2. 0 ≤ n
3. v : Δ(n)
4. i : ℕn + 2
5. ∀i:ℕn + 1. (r0 ≤ (v i))
6. Σ{v i | 0≤i≤n} = r1
7. ∀i@0:ℕ(n + 1) + 1. (r0 ≤ if i@0 <z i then v i@0 if i <z i@0 then v (i@0 - 1) else r0 fi )
⊢ Σ{if i@0 <z i then v i@0 if i <z i@0 then v (i@0 - 1) else r0 fi  | 0≤i@0≤n + 1} = r1

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  v  :  \mDelta{}(n)
3.  i  :  \mBbbN{}n  +  2
4.  0  \mleq{}  n
5.  \mforall{}i:\mBbbN{}n  +  1.  (r0  \mleq{}  (v  i))
6.  \mSigma{}\{v  i  |  0\mleq{}i\mleq{}n\}  =  r1
7.  \mforall{}i@0:\mBbbN{}(n  +  1)  +  1.  (r0  \mleq{}  if  i@0  <z  i  then  v  i@0  if  i  <z  i@0  then  v  (i@0  -  1)  else  r0  fi  )
\mvdash{}  \mSigma{}\{if  i@0  <z  i  then  v  i@0  if  i  <z  i@0  then  v  (i@0  -  1)  else  r0  fi    |  0\mleq{}i@0\mleq{}n  +  1\}  =  r1


By

---

Latex:
PromoteHyp  4  2

---

Home Index