Nuprl Definition : geo-pt-sep-from-line
geo-pt-sep-from-line(e; x; a; b) ==
(a ≠ x ∧ b ≠ x) ∧ (∀y:Point. (((y-a-b ⇒ y ≠ x) ∧ (a-b-y ⇒ y ≠ x)) ∧ (b-y-a ⇒ y ≠ x)))
Definitions occuring in Statement :
geo-strict-between: a-b-c,
geo-sep: a ≠ b,
geo-point: Point,
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q
Definitions occuring in definition :
all: ∀x:A. B[x],
geo-point: Point,
and: P ∧ Q,
implies: P ⇒ Q,
geo-strict-between: a-b-c,
geo-sep: a ≠ b
Latex:
geo-pt-sep-from-line(e; x; a; b) ==
(a \mneq{} x \mwedge{} b \mneq{} x) \mwedge{} (\mforall{}y:Point. (((y-a-b {}\mRightarrow{} y \mneq{} x) \mwedge{} (a-b-y {}\mRightarrow{} y \mneq{} x)) \mwedge{} (b-y-a {}\mRightarrow{} y \mneq{} x)))
Date html generated:
2017_10_02-PM-06_21_14
Last ObjectModification:
2017_08_05-PM-04_15_45
Theory : euclidean!plane!geometry
Home
Index