Nuprl Definition : geo-length-type
Length == x,y:{p:Point| O_X_p} //x ≡ y
Definitions occuring in Statement :
geo-X: X,
geo-O: O,
geo-eq: a ≡ b,
geo-between: a_b_c,
geo-point: Point,
quotient: x,y:A//B[x; y],
set: {x:A| B[x]}
Definitions occuring in definition :
quotient: x,y:A//B[x; y],
set: {x:A| B[x]} ,
geo-point: Point,
geo-between: a_b_c,
geo-O: O,
geo-X: X,
geo-eq: a ≡ b
FDL editor aliases :
geo-length-type
geo-length-type
Latex:
Length == x,y:\{p:Point| O\_X\_p\} //x \mequiv{} y
Date html generated:
2017_10_02-PM-04_45_17
Last ObjectModification:
2017_08_05-AM-09_09_41
Theory : euclidean!plane!geometry
Home
Index