Nuprl Definition : P_line-sep
P_line-sep(eu;L;M) == ∃P:P_point(eu). ((¬P_point-line-sep(eu;P;L)) ∧ P_point-line-sep(eu;P;M))
Definitions occuring in Statement :
P_point-line-sep: P_point-line-sep(e;P;L),
P_point: P_point(eu),
exists: ∃x:A. B[x],
not: ¬A,
and: P ∧ Q
Definitions occuring in definition :
exists: ∃x:A. B[x],
P_point: P_point(eu),
and: P ∧ Q,
not: ¬A,
P_point-line-sep: P_point-line-sep(e;P;L)
FDL editor aliases :
P_line-sep
Latex:
P\_line-sep(eu;L;M) == \mexists{}P:P\_point(eu). ((\mneg{}P\_point-line-sep(eu;P;L)) \mwedge{} P\_point-line-sep(eu;P;M))
Date html generated:
2019_10_16-PM-03_02_26
Last ObjectModification:
2018_08_08-PM-07_08_05
Theory : euclidean!plane!geometry
Home
Index