Nuprl Definition : geo-opp-side
P-AB-Q == (¬(∀T:Point. (P_T_Q ⇒ (¬Colinear(A;B;T))))) ∧ (¬Colinear(A;B;P)) ∧ (¬Colinear(A;B;Q))
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,
and: P ∧ Q
Definitions occuring in definition :
all: ∀x:A. B[x],
geo-point: Point,
implies: P ⇒ Q,
geo-between: a_b_c,
and: P ∧ Q,
not: ¬A,
geo-colinear: Colinear(a;b;c)
FDL editor aliases :
geo-opp-side
geo-opp-side
Latex:
P-AB-Q == (\mneg{}(\mforall{}T:Point. (P\_T\_Q {}\mRightarrow{} (\mneg{}Colinear(A;B;T))))) \mwedge{} (\mneg{}Colinear(A;B;P)) \mwedge{} (\mneg{}Colinear(A;B;Q))
Date html generated:
2017_10_02-PM-06_21_23
Last ObjectModification:
2017_08_05-PM-04_15_54
Theory : euclidean!plane!geometry
Home
Index