---

Step * of Lemma mon_itop_split_el

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

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

---

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])  *  (E[b]  *  (\mPi{}  b  +  1  \mleq{}  j  <  c.  E[j])))))  supposing 
          (b  <  c  and 
          (a  \mleq{}  b))


By

---

Latex:
((UnivCD)  THENA  Auto)

---

Home Index