Nuprl Definition : rv-sep-witness
rv-sep-witness(rv;x;y) ==
case rv."+sep" -y -y x y
case rv."#or" -y + x 0 -y + x
case rv."#or" x + -y 0 -y + x
let _,p = rv."positive" x - y
in p ((((rlessw(r0^2;||x - y||^2) * 20) + 1) * 20) + 1)
of inl(_) =>
Ax
| inr(b) =>
case rv."#or" 0 -y + x 0 b of inl(_) => Ax | inr(a) => a
of inl(_) =>
Ax
| inr(b) =>
case rv."#or" 0 -y + x -y + y b of inl(_) => Ax | inr(a) => a
of inl(_) =>
Ax
| inr(a) =>
a
Definitions occuring in Statement :
rv-norm: ||x||,
rv-sub: x - y,
rv-minus: -x,
rv-add: x + y,
rv-0: 0,
rlessw: rlessw(x;y),
rnexp: x^k1,
int-to-real: r(n),
apply: f a,
spread: spread def,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
multiply: n * m,
add: n + m,
natural_number: $n,
token: "$token",
axiom: Ax,
record-select: r.x
Definitions occuring in definition :
axiom: Ax,
rv-minus: -x,
rv-add: x + y,
rv-0: 0,
token: "$token",
record-select: r.x,
apply: f a,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
natural_number: $n,
rv-sub: x - y,
rv-norm: ||x||,
rnexp: x^k1,
int-to-real: r(n),
rlessw: rlessw(x;y),
multiply: n * m,
add: n + m,
spread: spread def
FDL editor aliases :
rv-sep-witness
Latex:
rv-sep-witness(rv;x;y) ==
case rv."+sep" -y -y x y
case rv."\#or" -y + x 0 -y + x
case rv."\#or" x + -y 0 -y + x
let $_{}$,p = rv."positive" x - y
in p ((((rlessw(r0\^{}2;||x - y||\^{}2) * 20) + 1) * 20) + 1)
of inl($_{}$) =>
Ax
| inr(b) =>
case rv."\#or" 0 -y + x 0 b of inl($_{}$) => Ax | inr(a) => a
of inl($_{}$) =>
Ax
| inr(b) =>
case rv."\#or" 0 -y + x -y + y b of inl($_{}$) => Ax | inr(a) => a
of inl($_{}$) =>
Ax
| inr(a) =>
a
Date html generated:
2016_11_08-AM-09_16_39
Last ObjectModification:
2016_11_03-AM-10_53_40
Theory : inner!product!spaces
Home
Index