Nuprl Definition : r2-eu-prim
r2-eu-prim() ==  Point=ℝ^2 O=λa,b,c,d. (d(c;d) < d(a;b)) Left=λa,b,c. r2-left(a;b;c)
Definitions occuring in Statement : 
r2-left: r2-left(p;q;r)
, 
real-vec-dist: d(x;y)
, 
real-vec: ℝ^n
, 
rless: x < y
, 
mk-eu-prim: mk-eu-prim, 
lambda: λx.A[x]
, 
natural_number: $n
FDL editor aliases : 
r2-eu-prim
Latex:
r2-eu-prim()  ==    Point=\mBbbR{}\^{}2  O=\mlambda{}a,b,c,d.  (d(c;d)  <  d(a;b))  Left=\mlambda{}a,b,c.  r2-left(a;b;c)
Date html generated:
2020_05_20-PM-01_10_19
Last ObjectModification:
2019_12_11-AM-11_14_54
Theory : reals!model!euclidean!geometry
Home
Index