### Nuprl Lemma : free_abmon_umap_wf

`∀S:DSet. ∀f:FAbMon(S).`
`  (f.umap ∈ mon':AbMon ⟶ f':(|S| ⟶ |mon'|) ⟶ {!g:MonHom(f.mon,mon') | (g o f.inj) = f' ∈ (|S| ⟶ |mon'|)})`

Proof

Definitions occuring in Statement :  free_abmon_umap: `f.umap` free_abmon_inj: `f.inj` free_abmon_mon: `f.mon` free_abmonoid: `FAbMon(S)` compose: `f o g` unique_set: `{!x:T | P[x]}` all: `∀x:A. B[x]` member: `t ∈ T` function: `x:A ⟶ B[x]` equal: `s = t ∈ T` monoid_hom: `MonHom(M1,M2)` abmonoid: `AbMon` grp_car: `|g|` dset: `DSet` set_car: `|p|`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` free_abmonoid: `FAbMon(S)` free_abmon_umap: `f.umap` free_abmon_inj: `f.inj` free_abmon_mon: `f.mon` pi1: `fst(t)` pi2: `snd(t)`
Lemmas referenced :  free_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{}f:FAbMon(S).
(f.umap  \mmember{}  mon':AbMon  {}\mrightarrow{}  f':(|S|  {}\mrightarrow{}  |mon'|)  {}\mrightarrow{}  \{!g:MonHom(f.mon,mon')  |  (g  o  f.inj)  =  f'\})

Date html generated: 2016_05_16-AM-07_48_29
Last ObjectModification: 2015_12_28-PM-06_02_14

Theory : mset

Home Index