Nuprl Definition : rev_perm
↔p{n} == mk_perm(rev_permf(n);rev_permf(n))
Definitions occuring in Statement :
rev_permf: rev_permf(n),
mk_perm: mk_perm(f;b)
Definitions occuring in definition :
mk_perm: mk_perm(f;b),
rev_permf: rev_permf(n)
Latex:
\mrightleftharpoons{}p\{n\} == mk\_perm(rev\_permf(n);rev\_permf(n))
Date html generated:
2016_05_16-AM-07_30_27
Last ObjectModification:
2015_09_23-AM-09_51_20
Theory : perms_1
Home
Index