---

Step * of Lemma mon_itop_split

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

---

Latex:

---

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


By

---

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

---

Home Index