---

Step * 1 1 of Lemma mon_for_eq_itop


1. g : IMonoid
2. A : Type
3. as : A List
4. f : A ⟶ |g|
⊢ (Π map(λx:A. f[x];as)) = (Π 0 ≤ i < ||as||. f[as[i]]) ∈ |g|
BY
{ (RWO "mon_reduce_eq_itop" 0 THENA Auto) }

1
1. g : IMonoid
2. A : Type
3. as : A List
4. f : A ⟶ |g|
⊢ (Π 0 ≤ i < ||map(λx:A. f[x];as)||. map(λx:A. f[x];as)[i]) = (Π 0 ≤ i < ||as||. f[as[i]]) ∈ |g|

---

Latex:

---

Latex:

1.  g  :  IMonoid
2.  A  :  Type
3.  as  :  A  List
4.  f  :  A  {}\mrightarrow{}  |g|
\mvdash{}  (\mPi{}  map(\mlambda{}x:A.  f[x];as))  =  (\mPi{}  0  \mleq{}  i  <  ||as||.  f[as[i]])


By

---

Latex:
(RWO  "mon\_reduce\_eq\_itop"  0  THENA  Auto)

---

Home Index