Nuprl Definition : fg-hom
fg-hom(G;f;w) ==
accumulate (with value x and list item u):
x * case u of inl(a) => f a | inr(b) => ~ (f b)
over list:
w
with starting value:
e)
Definitions occuring in Statement :
list_accum: list_accum,
infix_ap: x f y,
apply: f a,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
grp_inv: ~,
grp_id: e,
grp_op: *
Definitions occuring in definition :
list_accum: list_accum,
infix_ap: x f y,
grp_op: *,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
grp_inv: ~,
apply: f a,
grp_id: e
FDL editor aliases :
fg-hom
Latex:
fg-hom(G;f;w) ==
accumulate (with value x and list item u):
x * case u of inl(a) => f a | inr(b) => \msim{} (f b)
over list:
w
with starting value:
e)
Date html generated:
2020_05_20-AM-08_22_59
Last ObjectModification:
2017_01_15-PM-06_21_45
Theory : free!groups
Home
Index