Step
*
of Lemma
mcopower_inj_is_hom
∀s:DSet. ∀g:AbMon. ∀c:MCopower(s;g). ∀j:|s|. IsMonHom{g,c.mon}(c.inj j)
BY
{ ((RepD
THENM AssertLemma `mcopower_properties` []
THENM Unfold `uni_sat` (-1)
THENM BHyp (-1)) THEN Auto) }
Latex:
Latex:
\mforall{}s:DSet. \mforall{}g:AbMon. \mforall{}c:MCopower(s;g). \mforall{}j:|s|. IsMonHom\{g,c.mon\}(c.inj j)
By
Latex:
((RepD
THENM AssertLemma `mcopower\_properties` []
THENM Unfold `uni\_sat` (-1)
THENM BHyp (-1)) THEN Auto)
Home
Index