Nuprl Definition : geo-convex

IsConvex(x.P[x]) ==  ∀x,y,z:Point.  (x_y_z ⇒ P[x] ⇒ P[z] ⇒ P[y])


Definitions occuring in Statement :  geo-between: a_b_c,  geo-point: Point,  all: ∀x:A. B[x],  implies: P ⇒ Q
Definitions occuring in definition :  all: ∀x:A. B[x],  geo-point: Point,  geo-between: a_b_c,  implies: P ⇒ Q
FDL editor aliases :  geo-convex
Latex:
IsConvex(x.P[x])  ==    \mforall{}x,y,z:Point.    (x\_y\_z  {}\mRightarrow{}  P[x]  {}\mRightarrow{}  P[z]  {}\mRightarrow{}  P[y])


Date html generated: 2017_10_02-PM-06_48_45
Last ObjectModification: 2017_08_06-PM-07_28_28

Theory : euclidean!plane!geometry


Home Index