---

Step * of Lemma itop_shift

∀[g:IMonoid]. ∀[a,b:ℤ].
  ∀[E:{a..b-} ⟶ |g|]. ∀[k:ℤ].  (Π(*,e) a ≤ j < b. E[j] = Π(*,e) a + k ≤ j < b + k. E[j - k] ∈ |g|) supposing a ≤ b
BY
{ (Auto
   THEN Assert
        ∀b:ℤ. ∀E:{a..b-} ⟶ |g|. (Π(*,e) a ≤ j < b. E[j] = Π(*,e) a + k ≤ j < b + k. E[j - k] ∈ |g|) supposing a ≤ b⋅
   ) }

1
.....assertion..... 
1. g : IMonoid
2. a : ℤ
3. b : ℤ
4. a ≤ b
5. E : {a..b-} ⟶ |g|
6. k : ℤ
⊢ ∀b:ℤ. ∀E:{a..b-} ⟶ |g|. (Π(*,e) a ≤ j < b. E[j] = Π(*,e) a + k ≤ j < b + k. E[j - k] ∈ |g|) supposing a ≤ b

2
1. g : IMonoid
2. a : ℤ
3. b : ℤ
4. a ≤ b
5. E : {a..b-} ⟶ |g|
6. k : ℤ
7. ∀b:ℤ. ∀E:{a..b-} ⟶ |g|. (Π(*,e) a ≤ j < b. E[j] = Π(*,e) a + k ≤ j < b + k. E[j - k] ∈ |g|) supposing a ≤ b
⊢ Π(*,e) a ≤ j < b. E[j] = Π(*,e) a + k ≤ j < b + k. E[j - k] ∈ |g|

---

Latex:

---

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


By

---

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

---

Home Index