Nuprl Definition : vs-sum
Σs:S. V[s] == Point= s:S ⟶ Point(V[s]) zero= λs.0 x+y= λs.x s + y s k*u= λs.k * u s
Definitions occuring in Statement :
mk-vs: mk-vs,
vs-mul: a * x,
vs-add: x + y,
vs-0: 0,
vs-point: Point(vs),
apply: f a,
lambda: λx.A[x],
function: x:A ⟶ B[x]
Definitions occuring in definition :
mk-vs: mk-vs,
function: x:A ⟶ B[x],
vs-point: Point(vs),
vs-0: 0,
vs-add: x + y,
lambda: λx.A[x],
vs-mul: a * x,
apply: f a
FDL editor aliases :
vs-sum
Latex:
\mSigma{}s:S. V[s] == Point= s:S {}\mrightarrow{} Point(V[s]) zero= \mlambda{}s.0 x+y= \mlambda{}s.x s + y s k*u= \mlambda{}s.k * u s
Date html generated:
2018_05_22-PM-09_42_30
Last ObjectModification:
2017_11_09-PM-01_27_52
Theory : linear!algebra
Home
Index