Nuprl Definition : vec-midpoint
vec-midpoint(a;b) ==  (r1/r(2))*a + b
Definitions occuring in Statement : 
real-vec-mul: a*X
, 
real-vec-add: X + Y
, 
rdiv: (x/y)
, 
int-to-real: r(n)
, 
natural_number: $n
Definitions occuring in definition : 
real-vec-add: X + Y
, 
natural_number: $n
, 
int-to-real: r(n)
, 
rdiv: (x/y)
, 
real-vec-mul: a*X
FDL editor aliases : 
vec-midpoint
Latex:
vec-midpoint(a;b)  ==    (r1/r(2))*a  +  b
Date html generated:
2016_10_28-AM-07_42_31
Last ObjectModification:
2016_09_28-PM-04_07_51
Theory : reals!model!euclidean!geometry
Home
Index