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