Nuprl Definition : extend_perm
↑{n}(p) == mk_perm(extend_permf(p.f;n);extend_permf(p.b;n))
Definitions occuring in Statement :
extend_permf: extend_permf(pf;n),
mk_perm: mk_perm(f;b),
perm_b: p.b,
perm_f: p.f
Definitions occuring in definition :
mk_perm: mk_perm(f;b),
perm_f: p.f,
extend_permf: extend_permf(pf;n),
perm_b: p.b
Latex:
\muparrow{}\{n\}(p) == mk\_perm(extend\_permf(p.f;n);extend\_permf(p.b;n))
Date html generated:
2016_05_16-AM-07_31_11
Last ObjectModification:
2015_09_23-AM-09_51_24
Theory : perms_1
Home
Index