---

Step * of Lemma itop_split

∀[g:IMonoid]. ∀[a,b,c:ℤ].
  (∀[E:{a..c-} ⟶ |g|]. (Π(*,e) a ≤ j < c. E[j] = (Π(*,e) a ≤ j < b. E[j] * Π(*,e) b ≤ j < c. E[j]) ∈ |g|)) supposing 
     ((b ≤ c) and 
     (a ≤ b))
BY
{ RepeatMFor 4 (D 0) THENA Auto }

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

---

Latex:

---

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


By

---

Latex:
RepeatMFor  4  (D  0)  THENA  Auto

---

Home Index