Nuprl Definition : geo-parallel-points
geo-parallel-points(e;a;b;c;d) == (a ≠ b ∧ c ≠ d) ∧ (¬(∃x,y:{z:Point| Colinear(z;a;b)} . (x leftof cd ∧ y leftof dc)))
Definitions occuring in Statement :
geo-colinear: Colinear(a;b;c),
geo-left: a leftof bc,
geo-sep: a ≠ b,
geo-point: Point,
exists: ∃x:A. B[x],
not: ¬A,
and: P ∧ Q,
set: {x:A| B[x]}
Definitions occuring in definition :
geo-sep: a ≠ b,
not: ¬A,
exists: ∃x:A. B[x],
set: {x:A| B[x]} ,
geo-point: Point,
geo-colinear: Colinear(a;b;c),
and: P ∧ Q,
geo-left: a leftof bc
FDL editor aliases :
geo-parallel-points
Latex:
geo-parallel-points(e;a;b;c;d) ==
(a \mneq{} b \mwedge{} c \mneq{} d) \mwedge{} (\mneg{}(\mexists{}x,y:\{z:Point| Colinear(z;a;b)\} . (x leftof cd \mwedge{} y leftof dc)))
Date html generated:
2019_10_16-PM-01_45_49
Last ObjectModification:
2019_08_19-PM-02_51_09
Theory : euclidean!plane!geometry
Home
Index