Step
*
of Lemma
iseg_product-split
∀[i,j,k:ℤ]. (iseg_product(i;j) ~ iseg_product(i;k) * iseg_product(k + 1;j)) supposing (k < j and (i ≤ k) and (1 ≤ i))
BY
{ (Auto
THEN Unfold `iseg_product` 0
THEN (InstLemma `combinations-split` [⌜j⌝;⌜(k - i) + 1⌝;⌜(j - k + 1) + 1⌝]⋅ THENA Auto')
THEN (RW IntNormC (-1) THENM RW IntNormC 0)
THEN Auto') }
Latex:
Latex:
\mforall{}[i,j,k:\mBbbZ{}].
(iseg\_product(i;j) \msim{} iseg\_product(i;k) * iseg\_product(k + 1;j)) supposing
(k < j and
(i \mleq{} k) and
(1 \mleq{} i))
By
Latex:
(Auto
THEN Unfold `iseg\_product` 0
THEN (InstLemma `combinations-split` [\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}(k - i) + 1\mkleeneclose{};\mkleeneopen{}(j - k + 1) + 1\mkleeneclose{}]\mcdot{} THENA Auto')
THEN (RW IntNormC (-1) THENM RW IntNormC 0)
THEN Auto')
Home
Index