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