Step
*
of Lemma
rsum-split2
∀[n,m:ℤ]. ∀[k:{n..m + 1-}]. ∀[x:{n..m + 1-} ⟶ ℝ]. (Σ{x[i] | n≤i≤m} = (Σ{x[i] | n≤i≤k} + Σ{x[i] | k + 1≤i≤m}))
BY
{ (InstLemma `rsum-split` [] THEN RepeatFor 2 (ParallelLast') THEN Auto) }
Latex:
Latex:
\mforall{}[n,m:\mBbbZ{}]. \mforall{}[k:\{n..m + 1\msupminus{}\}]. \mforall{}[x:\{n..m + 1\msupminus{}\} {}\mrightarrow{} \mBbbR{}].
(\mSigma{}\{x[i] | n\mleq{}i\mleq{}m\} = (\mSigma{}\{x[i] | n\mleq{}i\mleq{}k\} + \mSigma{}\{x[i] | k + 1\mleq{}i\mleq{}m\}))
By
Latex:
(InstLemma `rsum-split` [] THEN RepeatFor 2 (ParallelLast') THEN Auto)
Home
Index