Nuprl Definition : geoline
LINE == l,m:Line//l ≡ m
Definitions occuring in Statement :
geo-line-eq: l ≡ m,
geo-line: Line,
quotient: x,y:A//B[x; y]
Definitions occuring in definition :
geo-line-eq: l ≡ m,
geo-line: Line,
quotient: x,y:A//B[x; y]
FDL editor aliases :
geoline
Latex:
LINE == l,m:Line//l \mequiv{} m
Date html generated:
2018_05_22-PM-01_02_45
Last ObjectModification:
2018_05_10-PM-04_30_26
Theory : euclidean!plane!geometry
Home
Index