Nuprl Definition : rn-ip
ipℝ^n == vs=vecℝ^n;ip=λx,y. x⋅y;positive=TERMOF{real-vec-sep-0-iff:o, 1:l} n;perp=TERMOF{real-vec-perp-exists:o, 1:l} n
Definitions occuring in Statement :
rv-n: vecℝ^n,
mk-inner-product-space: mk-inner-product-space,
dot-product: x⋅y,
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
mk-inner-product-space: mk-inner-product-space,
rv-n: vecℝ^n,
lambda: λx.A[x],
dot-product: x⋅y,
apply: f a
TermOfs occuring in Definition :
real-vec-perp-exists,
real-vec-sep-0-iff
FDL editor aliases :
rn-ip
Latex:
ip\mBbbR{}\^{}n ==
vs=vec\mBbbR{}\^{}n;
ip=\mlambda{}x,y. x\mcdot{}y;
positive=TERMOF\{real-vec-sep-0-iff:o, 1:l\} n;
perp=TERMOF\{real-vec-perp-exists:o, 1:l\} n
Date html generated:
2017_10_04-PM-11_50_57
Last ObjectModification:
2017_04_07-PM-04_33_55
Theory : inner!product!spaces
Home
Index