---

Step * of Lemma mon_itop_shift

∀[g:IMonoid]. ∀[a,b:ℤ].
  ∀[E:{a..b-} ⟶ |g|]. ∀[k:ℤ].  ((Π a ≤ j < b. E[j]) = (Π a + k ≤ j < b + k. E[j - k]) ∈ |g|) supposing a ≤ b
BY
{ ProveSpecializedLemma `itop_shift` 0 [parm{i}] (FoldC `mon_itop`) }

---

Latex:

---

Latex:
\mforall{}[g:IMonoid].  \mforall{}[a,b:\mBbbZ{}].
    \mforall{}[E:\{a..b\msupminus{}\}  {}\mrightarrow{}  |g|].  \mforall{}[k:\mBbbZ{}].    ((\mPi{}  a  \mleq{}  j  <  b.  E[j])  =  (\mPi{}  a  +  k  \mleq{}  j  <  b  +  k.  E[j  -  k])) 
    supposing  a  \mleq{}  b


By

---

Latex:
ProveSpecializedLemma  `itop\_shift`  0  [parm\{i\}]  (FoldC  `mon\_itop`)

---

Home Index