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 :  grp_id: e,  apply: f a,  grp_inv: ~,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  grp_op: *,  infix_ap: x f y,  list_accum: list_accum
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: 2017_01_19-PM-02_51_16
Last ObjectModification: 2017_01_15-PM-06_21_45

Theory : free!groups


Home Index