Step
*
1
1
2
1
1
1
1
of Lemma
simplex-face_wf
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 )
8. ¬(i = (n + 1) ∈ ℤ)
9. ∀[x:ℕ(n + 1) + 1 ⟶ ℝ]. (Σ{x[i] | 0≤i≤n + 1} = (Σ{x[i] | 0≤i≤i} + Σ{x[i] | i + 1≤i≤n + 1}))
10. Σ{if i@0 <z i then v i@0 if i <z i@0 then v (i@0 - 1) else r0 fi | i + 1≤i@0≤n + 1} = Σ{v (j - 1) | i + 1≤j≤n + 1}
11. Σ{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≤i}
= Σ{if (j =z i) then r0 else v j fi | 0≤j≤i}
12. Σ{if (j =z i) then r0 else v j fi | 0≤j≤i} = Σ{v j | 0≤j≤i - 1}
⊢ (Σ{v j | 0≤j≤i - 1} + Σ{v (j - 1) | i + 1≤j≤n + 1}) = r1
BY
{ ((InstLemma `rsum-shift` [⌜1⌝;⌜i + 1⌝;⌜n + 1⌝]⋅ THENM RWO "-1" 0) THENA Auto) }
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 )
8. ¬(i = (n + 1) ∈ ℤ)
9. ∀[x:ℕ(n + 1) + 1 ⟶ ℝ]. (Σ{x[i] | 0≤i≤n + 1} = (Σ{x[i] | 0≤i≤i} + Σ{x[i] | i + 1≤i≤n + 1}))
10. Σ{if i@0 <z i then v i@0 if i <z i@0 then v (i@0 - 1) else r0 fi | i + 1≤i@0≤n + 1} = Σ{v (j - 1) | i + 1≤j≤n + 1}
11. Σ{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≤i}
= Σ{if (j =z i) then r0 else v j fi | 0≤j≤i}
12. Σ{if (j =z i) then r0 else v j fi | 0≤j≤i} = Σ{v j | 0≤j≤i - 1}
13. ∀[x:Top]. (Σ{x[i] | i + 1≤i≤n + 1} ~ Σ{x[i + 1] | (i + 1) - 1≤i≤(n + 1) - 1})
⊢ (Σ{v j | 0≤j≤i - 1} + Σ{v ((j + 1) - 1) | (i + 1) - 1≤j≤(n + 1) - 1}) = r1
Latex:
Latex:
1. n : \mBbbZ{}
2. 0 \mleq{} n
3. v : \mDelta{}(n)
4. i : \mBbbN{}n + 2
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 )
8. \mneg{}(i = (n + 1))
9. \mforall{}[x:\mBbbN{}(n + 1) + 1 {}\mrightarrow{} \mBbbR{}]. (\mSigma{}\{x[i] | 0\mleq{}i\mleq{}n + 1\} = (\mSigma{}\{x[i] | 0\mleq{}i\mleq{}i\} + \mSigma{}\{x[i] | i + 1\mleq{}i\mleq{}n + 1\}))
10. \mSigma{}\{if i@0 <z i then v i@0
if i <z i@0 then v (i@0 - 1)
else r0
fi | i + 1\mleq{}i@0\mleq{}n + 1\}
= \mSigma{}\{v (j - 1) | i + 1\mleq{}j\mleq{}n + 1\}
11. \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{}i\}
= \mSigma{}\{if (j =\msubz{} i) then r0 else v j fi | 0\mleq{}j\mleq{}i\}
12. \mSigma{}\{if (j =\msubz{} i) then r0 else v j fi | 0\mleq{}j\mleq{}i\} = \mSigma{}\{v j | 0\mleq{}j\mleq{}i - 1\}
\mvdash{} (\mSigma{}\{v j | 0\mleq{}j\mleq{}i - 1\} + \mSigma{}\{v (j - 1) | i + 1\mleq{}j\mleq{}n + 1\}) = r1
By
Latex:
((InstLemma `rsum-shift` [\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}i + 1\mkleeneclose{};\mkleeneopen{}n + 1\mkleeneclose{}]\mcdot{} THENM RWO "-1" 0) THENA Auto)
Home
Index