Nuprl Lemma : mcopower_inj_wf

s:DSet. ∀g:AbMon. ∀m:mcopower_sig{i:l}(s;g).  (m.inj ∈ |s| ⟶ |g| ⟶ |m.mon|)


Proof




Definitions occuring in Statement :  mcopower_inj: m.inj mcopower_mon: m.mon mcopower_sig: mcopower_sig{i:l}(s;g) all: x:A. B[x] member: t ∈ T function: x:A ⟶ B[x] abmonoid: AbMon grp_car: |g| dset: DSet set_car: |p|
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T mcopower_sig: mcopower_sig{i:l}(s;g) mcopower_inj: m.inj mcopower_mon: m.mon pi1: fst(t) pi2: snd(t)
Lemmas referenced :  mcopower_sig_wf abmonoid_wf dset_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut sqequalHypSubstitution productElimination thin sqequalRule hypothesisEquality hypothesis lemma_by_obid dependent_functionElimination

Latex:
\mforall{}s:DSet.  \mforall{}g:AbMon.  \mforall{}m:mcopower\_sig\{i:l\}(s;g).    (m.inj  \mmember{}  |s|  {}\mrightarrow{}  |g|  {}\mrightarrow{}  |m.mon|)



Date html generated: 2016_05_16-AM-08_12_55
Last ObjectModification: 2015_12_28-PM-06_09_44

Theory : polynom_1


Home Index