Nuprl Definition : P_point
P_point(eu) == p:Point × l:Line × 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,
and: P ∧ Q,
product: x:A × B[x]
Definitions occuring in definition :
geo-point: Point,
product: x:A × B[x],
geo-line: Line,
and: P ∧ Q,
geo-incident: p I L,
geo-plsep: p # l
FDL editor aliases :
P_point
Latex:
P\_point(eu) == p:Point \mtimes{} l:Line \mtimes{} n:Line \mtimes{} (p I n \mwedge{} p \# l)
Date html generated:
2019_10_16-PM-02_59_19
Last ObjectModification:
2018_08_08-PM-05_57_54
Theory : euclidean!plane!geometry
Home
Index