Nuprl Definition : perm_morph
perm_morph(S;T;s2t;t2s;p) == mk_perm(s2t o (p.f o t2s);s2t o (p.b o t2s))
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:
perm\_morph(S;T;s2t;t2s;p) == mk\_perm(s2t o (p.f o t2s);s2t o (p.b o t2s))
Date html generated:
2016_05_16-AM-07_33_21
Last ObjectModification:
2015_09_23-AM-09_51_26
Theory : perms_2
Home
Index