Nuprl Definition : geo-parallel
geo-parallel(e;a;b;c;d) == (a ≠ b ∧ c ≠ d) ∧ (∀x:Point. (Colinear(a;b;x) ⇒ x # cd))
Definitions occuring in Statement :
geo-lsep: a # bc,
geo-colinear: Colinear(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 :
and: P ∧ Q,
geo-sep: a ≠ b,
all: ∀x:A. B[x],
geo-point: Point,
implies: P ⇒ Q,
geo-colinear: Colinear(a;b;c),
geo-lsep: a # bc
FDL editor aliases :
geo-parallel
Latex:
geo-parallel(e;a;b;c;d) == (a \mneq{} b \mwedge{} c \mneq{} d) \mwedge{} (\mforall{}x:Point. (Colinear(a;b;x) {}\mRightarrow{} x \# cd))
Date html generated:
2018_05_22-PM-00_13_02
Last ObjectModification:
2017_10_12-AM-11_02_09
Theory : euclidean!plane!geometry
Home
Index