Nuprl Definition : pgeo-primitives
ProjGeomPrimitives == "Point":Type"Line":Type"PS":Point ⟶ Line ⟶ ℙ
Definitions occuring in Statement :
pgeo-line: Line,
pgeo-point: Point,
top: Top,
prop: ℙ,
function: x:A ⟶ B[x],
token: "$token",
universe: Type,
record+: record+,
record: record(x.T[x])
Definitions occuring in definition :
record+: record+,
record: record(x.T[x]),
top: Top,
universe: Type,
token: "$token",
pgeo-point: Point,
function: x:A ⟶ B[x],
pgeo-line: Line,
prop: ℙ
FDL editor aliases :
pgeo-primitives
Latex:
ProjGeomPrimitives == "Point":Type"Line":Type"PS":Point {}\mrightarrow{} Line {}\mrightarrow{} \mBbbP{}
Date html generated:
2018_05_22-PM-00_22_14
Last ObjectModification:
2017_10_20-AM-11_59_02
Theory : euclidean!plane!geometry
Home
Index