Step * 1 1 of Lemma mset_fmon_wf


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

1
1. DSet
2. AbMon
3. |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. DSet
2. AbMon
3. |s| ⟶ |m|
⊢ 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