Nuprl Lemma : mcopower_inj_is_hom

s:DSet. ∀g:AbMon. ∀c:MCopower(s;g). ∀j:|s|.  IsMonHom{g,c.mon}(c.inj j)


Proof




Definitions occuring in Statement :  mcopower: MCopower(s;g) mcopower_inj: m.inj mcopower_mon: m.mon all: x:A. B[x] apply: a monoid_hom_p: IsMonHom{M1,M2}(f) abmonoid: AbMon dset: DSet set_car: |p|
Definitions unfolded in proof :  all: x:A. B[x] uni_sat: !x:T. Q[x] member: t ∈ T and: P ∧ Q uall: [x:A]. B[x] dset: DSet
Lemmas referenced :  mcopower_properties set_car_wf mcopower_wf abmonoid_wf dset_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution sqequalRule hypothesis dependent_functionElimination thin hypothesisEquality productElimination isectElimination setElimination rename

Latex:
\mforall{}s:DSet.  \mforall{}g:AbMon.  \mforall{}c:MCopower(s;g).  \mforall{}j:|s|.    IsMonHom\{g,c.mon\}(c.inj  j)



Date html generated: 2016_05_16-AM-08_13_05
Last ObjectModification: 2015_12_28-PM-06_09_48

Theory : polynom_1


Home Index