Nuprl Definition : perm_igrp
perm_igrp(T) == mk_igrp(Perm(T);λp,q. p O q;id_perm();λp.inv_perm(p))
Definitions occuring in Statement :
comp_perm: comp_perm,
inv_perm: inv_perm(p),
id_perm: id_perm(),
perm: Perm(T),
lambda: λx.A[x],
mk_igrp: mk_igrp(T;op;id;inv)
Definitions occuring in definition :
mk_igrp: mk_igrp(T;op;id;inv),
perm: Perm(T),
comp_perm: comp_perm,
id_perm: id_perm(),
lambda: λx.A[x],
inv_perm: inv_perm(p)
Latex:
perm\_igrp(T) == mk\_igrp(Perm(T);\mlambda{}p,q. p O q;id\_perm();\mlambda{}p.inv\_perm(p))
Date html generated:
2016_05_16-AM-07_29_07
Last ObjectModification:
2015_09_23-AM-09_51_15
Theory : perms_1
Home
Index