Nuprl Definition : seteqinv
seteqinv() == λ_,f,eq,moves. let u,v = eq λp.let u,v = p in <v, u> o moves in <v, u>
Definitions occuring in Statement :
seq-comp: f o s,
apply: f a,
lambda: λx.A[x],
spread: spread def,
pair: <a, b>
Definitions occuring in definition :
pair: <a, b>,
spread: spread def,
lambda: λx.A[x],
seq-comp: f o s,
apply: f a
FDL editor aliases :
seteqinv
Latex:
seteqinv() == \mlambda{}$_{}$,f,eq,moves. let u,v = eq \mlambda{}p.let u,v = p in <v, u> o moves \000Cin <v, u>
Date html generated:
2018_07_29-AM-09_51_07
Last ObjectModification:
2018_07_11-PM-00_07_36
Theory : constructive!set!theory
Home
Index