Nuprl Definition : P_line
P_line(eu) == l:Line × p:Point × n:{n:Line| p I n} × p # l
Definitions occuring in Statement :
geo-plsep: p # l,
geo-incident: p I L,
geo-line: Line,
geo-point: Point,
set: {x:A| B[x]} ,
product: x:A × B[x]
Definitions occuring in definition :
geo-point: Point,
product: x:A × B[x],
set: {x:A| B[x]} ,
geo-line: Line,
geo-incident: p I L,
geo-plsep: p # l
FDL editor aliases :
P_line
Latex:
P\_line(eu) == l:Line \mtimes{} p:Point \mtimes{} n:\{n:Line| p I n\} \mtimes{} p \# l
Date html generated:
2019_10_16-PM-02_59_56
Last ObjectModification:
2018_08_08-PM-05_59_36
Theory : euclidean!plane!geometry
Home
Index