---

Step * 1 of Lemma itop_shift

.....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
BY
{ BackThruLemma `int_le_to_int_upper` THENA Auto' }

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

---

Latex:

---

Latex:
.....assertion..... 
1.  g  :  IMonoid
2.  a  :  \mBbbZ{}
3.  b  :  \mBbbZ{}
4.  a  \mleq{}  b
5.  E  :  \{a..b\msupminus{}\}  {}\mrightarrow{}  |g|
6.  k  :  \mBbbZ{}
\mvdash{}  \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


By

---

Latex:
BackThruLemma  `int\_le\_to\_int\_upper`  THENA  Auto'

---

Home Index