Nuprl Definition : mk-real-vector-space
ss=ss;0=z;+=p;*=m;+sep=psep;*sep=msep == ss["0" := z]["+" := p]["*" := m]["+sep" := psep]["*sep" := msep]
Definitions occuring in Statement :
token: "$token",
record-update: r[x := v]
Definitions occuring in definition :
record-update: r[x := v],
token: "$token"
FDL editor aliases :
mk-real-vector-space
Latex:
ss=ss;
0=z;
+=p;
*=m;
+sep=psep;
*sep=msep ==
ss["0" := z]["+" := p]["*" := m]["+sep" := psep]["*sep" := msep]
Date html generated:
2017_10_04-PM-11_50_10
Last ObjectModification:
2017_06_22-PM-06_44_08
Theory : inner!product!spaces
Home
Index