Nuprl Definition : eu-pp-prim
pp(eu) == points=Point + Line lines=Line? plsep=λp,l. pp-sep(eu;p;l)
Definitions occuring in Statement :
pp-sep: pp-sep(eu;p;l),
geo-line: Line,
mk-pgeo-prim: mk-pgeo-prim,
geo-point: Point,
unit: Unit,
lambda: λx.A[x],
union: left + right
Definitions occuring in definition :
pp-sep: pp-sep(eu;p;l),
lambda: λx.A[x],
unit: Unit,
geo-line: Line,
union: left + right,
geo-point: Point,
mk-pgeo-prim: mk-pgeo-prim
FDL editor aliases :
eu-pp-prim
Latex:
pp(eu) == points=Point + Line lines=Line? plsep=\mlambda{}p,l. pp-sep(eu;p;l)
Date html generated:
2018_05_22-PM-01_16_43
Last ObjectModification:
2018_05_21-PM-03_40_03
Theory : euclidean!plane!geometry
Home
Index