---

Step * 1 of Lemma mon_for_eq_itop


1. g : IMonoid
2. A : Type
3. as : A List
4. f : A ⟶ |g|
⊢ (For{g} x ∈ as. f[x]) = (Π 0 ≤ i < ||as||. f[as[i]]) ∈ |g|
BY
{ (RepUnfolds ``mon_for for`` 0 THEN Fold `mon_reduce` 0) }

1
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|

---

Latex:

---

Latex:

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


By

---

Latex:
(RepUnfolds  ``mon\_for  for``  0  THEN  Fold  `mon\_reduce`  0)

---

Home Index