Nuprl Definition : rvlinecircle0
rvlinecircle0(n;a;b;p;q) ==
<p + quadratic1(d(q - a;p - a)^2;r(2) * p - a⋅q - a - p - a;||p - a||^2 - d(a;b)^2)*q - a - p - a
, p + quadratic2(d(q - a;p - a)^2;r(2) * p - a⋅q - a - p - a;||p - a||^2 - d(a;b)^2)*q - a - p - a
>
Definitions occuring in Statement :
real-vec-dist: d(x;y),
real-vec-norm: ||x||,
dot-product: x⋅y,
real-vec-mul: a*X,
real-vec-sub: X - Y,
real-vec-add: X + Y,
quadratic2: quadratic2(a;b;c),
quadratic1: quadratic1(a;b;c),
rnexp: x^k1,
rsub: x - y,
rmul: a * b,
int-to-real: r(n),
pair: <a, b>,
natural_number: $n
Definitions occuring in definition :
pair: <a, b>,
quadratic1: quadratic1(a;b;c),
real-vec-add: X + Y,
real-vec-mul: a*X,
quadratic2: quadratic2(a;b;c),
rmul: a * b,
int-to-real: r(n),
dot-product: x⋅y,
rsub: x - y,
real-vec-norm: ||x||,
rnexp: x^k1,
real-vec-dist: d(x;y),
natural_number: $n,
real-vec-sub: X - Y
FDL editor aliases :
rvlinecircle0
Latex:
rvlinecircle0(n;a;b;p;q) ==
<p + quadratic1(d(q - a;p - a)\^{}2;r(2) * p - a\mcdot{}q - a - p - a;||p - a||\^{}2 - d(a;b)\^{}2)*q - a - p - a
, p + quadratic2(d(q - a;p - a)\^{}2;r(2) * p - a\mcdot{}q - a - p - a;||p - a||\^{}2 - d(a;b)\^{}2)*q - a - p - a
>
Date html generated:
2018_05_22-PM-02_33_50
Last ObjectModification:
2018_03_22-AM-10_33_41
Theory : reals
Home
Index