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