Step
*
1
of Lemma
mon_itop_split_el
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|
BY
{ RWN 1 (LemmaWithC [`b',b] `mon_itop_split`) 0
THENM RWN 2 (LemmaC `mon_itop_unroll_lo`) 0
THEN Auto }
Latex:
Latex:
1. g : IMonoid
2. a : \mBbbZ{}
3. b : \mBbbZ{}
4. c : \mBbbZ{}
5. a \mleq{} b
6. b < c
7. E : \{a..c\msupminus{}\} {}\mrightarrow{} |g|
\mvdash{} (\mPi{} a \mleq{} j < c. E[j]) = ((\mPi{} a \mleq{} j < b. E[j]) * (E[b] * (\mPi{} b + 1 \mleq{} j < c. E[j])))
By
Latex:
RWN 1 (LemmaWithC [`b',b] `mon\_itop\_split`) 0
THENM RWN 2 (LemmaC `mon\_itop\_unroll\_lo`) 0
THEN Auto
Home
Index