Nuprl Definition : r3-dp-prim
r3-dp-prim() == (vec={v:ℝ^3| v ≠ λi.r0} , sep=λa,b. (a x b) ≠ λi.r0, perp=λa,b. (a⋅b = r0))
Definitions occuring in Statement :
rcp: (a x b),
real-vec-sep: a ≠ b,
dot-product: x⋅y,
real-vec: ℝ^n,
req: x = y,
int-to-real: r(n),
set: {x:A| B[x]} ,
lambda: λx.A[x],
natural_number: $n,
mk-dp-prim: (vec=V, sep=S, perp=P)
Definitions occuring in definition :
natural_number: $n,
int-to-real: r(n),
dot-product: x⋅y,
req: x = y,
lambda: λx.A[x],
rcp: (a x b),
real-vec-sep: a ≠ b,
real-vec: ℝ^n,
set: {x:A| B[x]} ,
mk-dp-prim: (vec=V, sep=S, perp=P)
FDL editor aliases :
r3-dp-prim
Latex:
r3-dp-prim() == (vec=\{v:\mBbbR{}\^{}3| v \mneq{} \mlambda{}i.r0\} , sep=\mlambda{}a,b. (a x b) \mneq{} \mlambda{}i.r0, perp=\mlambda{}a,b. (a\mcdot{}b = r0))
Date html generated:
2018_05_22-PM-02_43_43
Last ObjectModification:
2018_05_09-PM-01_42_32
Theory : reals
Home
Index