Nuprl Definition : comp_perm
p O q == mk_perm(p.f o q.f;q.b o p.b)
Definitions occuring in Statement :
mk_perm: mk_perm(f;b),
perm_b: p.b,
perm_f: p.f,
compose: f o g
Definitions occuring in definition :
mk_perm: mk_perm(f;b),
perm_f: p.f,
compose: f o g,
perm_b: p.b
Latex:
p O q == mk\_perm(p.f o q.f;q.b o p.b)
Date html generated:
2016_05_16-AM-07_28_45
Last ObjectModification:
2015_09_23-AM-09_51_14
Theory : perms_1
Home
Index