Nuprl Definition : free_abmonoid
FAbMon(S) ==
mon:AbMon
× inj:|S| ⟶ |mon|
× (mon':AbMon ⟶ f':(|S| ⟶ |mon'|) ⟶ {!g:MonHom(mon,mon') | (g o inj) = f' ∈ (|S| ⟶ |mon'|)})
Definitions occuring in Statement :
compose: f o g
,
unique_set: {!x:T | P[x]}
,
function: x:A ⟶ B[x]
,
product: x:A × B[x]
,
equal: s = t ∈ T
,
monoid_hom: MonHom(M1,M2)
,
abmonoid: AbMon
,
grp_car: |g|
,
set_car: |p|
Definitions occuring in definition :
product: x:A × B[x]
,
abmonoid: AbMon
,
unique_set: {!x:T | P[x]}
,
monoid_hom: MonHom(M1,M2)
,
equal: s = t ∈ T
,
function: x:A ⟶ B[x]
,
set_car: |p|
,
grp_car: |g|
,
compose: f o g
Latex:
FAbMon(S) ==
mon:AbMon
\mtimes{} inj:|S| {}\mrightarrow{} |mon|
\mtimes{} (mon':AbMon {}\mrightarrow{} f':(|S| {}\mrightarrow{} |mon'|) {}\mrightarrow{} \{!g:MonHom(mon,mon') | (g o inj) = f'\})
Date html generated:
2016_05_16-AM-07_48_16
Last ObjectModification:
2015_09_23-AM-09_52_06
Theory : mset
Home
Index