Nuprl Definition : geo-same-side
A,B-PQ == ∀T:Point. (A_T_B ⇒ (¬Colinear(P;Q;T)))
Definitions occuring in Statement :
geo-colinear: Colinear(a;b;c),
geo-between: a_b_c,
geo-point: Point,
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q
Definitions occuring in definition :
all: ∀x:A. B[x],
geo-point: Point,
implies: P ⇒ Q,
geo-between: a_b_c,
not: ¬A,
geo-colinear: Colinear(a;b;c)
FDL editor aliases :
geo-same-side
geo-same-side
Latex:
A,B-PQ == \mforall{}T:Point. (A\_T\_B {}\mRightarrow{} (\mneg{}Colinear(P;Q;T)))
Date html generated:
2017_10_02-PM-06_21_59
Last ObjectModification:
2017_08_05-PM-04_16_18
Theory : euclidean!plane!geometry
Home
Index