Nuprl Definition : mk-inner-product-space
vs=vs;ip=ip;positive=pos;perp=perp == vs["ip" := ip]["positive" := pos]["perp" := perp]
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-inner-product-space
Latex:
vs=vs;ip=ip;positive=pos;perp=perp == vs["ip" := ip]["positive" := pos]["perp" := perp]
Date html generated:
2017_10_04-PM-11_50_43
Last ObjectModification:
2017_04_07-PM-02_58_19
Theory : inner!product!spaces
Home
Index