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