Nuprl Definition : pgeo-dual-prim
pg* ==  points=Line lines=Point plsep=λl,p. p ≠ l
Definitions occuring in Statement : 
pgeo-plsep: a ≠ b
, 
mk-pgeo-prim: mk-pgeo-prim, 
pgeo-line: Line
, 
pgeo-point: Point
, 
lambda: λx.A[x]
Definitions occuring in definition : 
mk-pgeo-prim: mk-pgeo-prim, 
pgeo-line: Line
, 
pgeo-point: Point
, 
lambda: λx.A[x]
, 
pgeo-plsep: a ≠ b
FDL editor aliases : 
pgeo-dual-prim
Latex:
pg*  ==    points=Line  lines=Point  plsep=\mlambda{}l,p.  p  \mneq{}  l
Date html generated:
2018_05_22-PM-00_23_29
Last ObjectModification:
2017_10_31-PM-00_10_42
Theory : euclidean!plane!geometry
Home
Index