Nuprl Definition : pgeo-dual
pg* ==
mk-pgeo(pg*;
λp,l. (pg."Ssquashstable" l p);
pg."LPSepOr";
pg."PLSepOr";
pg."meet";
pg."join";
pg."three-lines";
pg."three-points")
Definitions occuring in Statement :
mk-pgeo: mk-pgeo(p; ss; por; lor; j; m; p3; l3),
pgeo-dual-prim: pg*,
apply: f a,
lambda: λx.A[x],
token: "$token",
record-select: r.x
Definitions occuring in definition :
mk-pgeo: mk-pgeo(p; ss; por; lor; j; m; p3; l3),
pgeo-dual-prim: pg*,
lambda: λx.A[x],
apply: f a,
record-select: r.x,
token: "$token"
FDL editor aliases :
pgeo-dual
Latex:
pg* ==
mk-pgeo(pg*;
\mlambda{}p,l. (pg."Ssquashstable" l p);
pg."LPSepOr";
pg."PLSepOr";
pg."meet";
pg."join";
pg."three-lines";
pg."three-points")
Date html generated:
2018_05_22-PM-00_28_24
Last ObjectModification:
2017_11_26-PM-02_06_31
Theory : euclidean!plane!geometry
Home
Index