---

Step * 1 1 of Lemma mset_fmon_wf


1. s : DSet
2. m : AbMon
3. f : |s| ⟶ |m|
⊢ λy:MSet{s}. msFor{m} z ∈ y
                (f z) ∈ MonHom(mset_mon{s},m)
BY
{ % Check umap is a homomorphism % 
 
((MemTypeCD) THEN Auto) 
THEN AbEval ``monoid_hom_p fun_thru_2op`` 0 
THEN ((GenUnivCD) THENA Auto) 
 }

1
1. s : DSet
2. m : AbMon
3. f : |s| ⟶ |m|
4. a1 : MSet{s}
5. a2 : MSet{s}
⊢ (msFor{m} z ∈ a1 + a2. (f z)) = ((msFor{m} z ∈ a1. (f z)) * (msFor{m} z ∈ a2. (f z))) ∈ |m|

2
1. s : DSet
2. m : AbMon
3. f : |s| ⟶ |m|
⊢ e = e ∈ |m|

---

Latex:

---

Latex:

1.  s  :  DSet
2.  m  :  AbMon
3.  f  :  |s|  {}\mrightarrow{}  |m|
\mvdash{}  \mlambda{}y:MSet\{s\}.  msFor\{m\}  z  \mmember{}  y
                                (f  z)  \mmember{}  MonHom(mset\_mon\{s\},m)


By

---

Latex:
\%  Check  umap  is  a  homomorphism  \% 
 
((MemTypeCD)  THEN  Auto) 
THEN  AbEval  ``monoid\_hom\_p  fun\_thru\_2op``  0 
THEN  ((GenUnivCD)  THENA  Auto) 

---

Home Index