Nuprl Definition : rv-add
x + y == rv."+" x y
Wellformedness Lemmas :
rv-add_wf
Definitions occuring in Statement :
apply: f a,
token: "$token",
record-select: r.x
Definitions occuring in definition :
apply: f a,
record-select: r.x,
token: "$token"
FDL editor aliases :
rv-add
Latex:
x + y == rv."+" x y
Date html generated:
2017_10_04-PM-11_50_15
Last ObjectModification:
2017_06_22-PM-06_44_12
Theory : inner!product!spaces
Home
Index