Nuprl Definition : geo-intersect-points
ab \/ cd ==  a ≠ b ∧ (∃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]
, 
and: P ∧ Q
, 
set: {x:A| B[x]} 
Definitions occuring in definition : 
geo-sep: a ≠ b
, 
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-intersect-points
Latex:
ab  \mbackslash{}/  cd  ==    a  \mneq{}  b  \mwedge{}  (\mexists{}x,y:\{z:Point|  Colinear(z;a;b)\}  .  (x  leftof  cd  \mwedge{}  y  leftof  dc))
Date html generated:
2019_10_16-PM-01_44_45
Last ObjectModification:
2019_06_20-AM-11_26_57
Theory : euclidean!plane!geometry
Home
Index