Nuprl Definition : rv-n
vecℝ^n ==
ss=sepℝ^n;
0=λi.r0;
+=λx,y. x + y;
*=λa,y. a*y;
+sep=TERMOF{real-vec-sep-add:o, 1:l} n;
*sep=TERMOF{real-vec-sep-mul:o, 1:l} n
Definitions occuring in Statement :
rn-ss: sepℝ^n,
mk-real-vector-space: mk-real-vector-space,
real-vec-mul: a*X,
real-vec-add: X + Y,
int-to-real: r(n),
apply: f a,
lambda: λx.A[x],
natural_number: $n
Definitions occuring in definition :
mk-real-vector-space: mk-real-vector-space,
rn-ss: sepℝ^n,
int-to-real: r(n),
natural_number: $n,
real-vec-add: X + Y,
lambda: λx.A[x],
real-vec-mul: a*X,
real-vec-sep-add,
apply: f a,
real-vec-sep-mul
TermOfs occuring in Definition :
real-vec-sep-mul,
real-vec-sep-add
FDL editor aliases :
rv-n
Latex:
vec\mBbbR{}\^{}n ==
ss=sep\mBbbR{}\^{}n;
0=\mlambda{}i.r0;
+=\mlambda{}x,y. x + y;
*=\mlambda{}a,y. a*y;
+sep=TERMOF\{real-vec-sep-add:o, 1:l\} n;
*sep=TERMOF\{real-vec-sep-mul:o, 1:l\} n
Date html generated:
2017_10_04-PM-11_50_53
Last ObjectModification:
2017_04_07-PM-02_47_03
Theory : inner!product!spaces
Home
Index