Nuprl Definition : name-morph-flip
flip(f;y) == λn.if eq-cname(n;y) then 1 - f n else f n fi
Definitions occuring in Statement :
eq-cname: eq-cname(x;y),
ifthenelse: if b then t else f fi ,
apply: f a,
lambda: λx.A[x],
subtract: n - m,
natural_number: $n
Definitions occuring in definition :
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
eq-cname: eq-cname(x;y),
subtract: n - m,
natural_number: $n,
apply: f a
FDL editor aliases :
name-morph-flip
Latex:
flip(f;y) == \mlambda{}n.if eq-cname(n;y) then 1 - f n else f n fi
Date html generated:
2016_06_16-PM-05_35_03
Last ObjectModification:
2015_09_23-AM-09_29_48
Theory : cubical!sets
Home
Index