Nuprl Definition : PlayfairPP
PlayfairPP(eu) ==
∀a0,a1,b0,b1,c0,c1,p:Point.
((geo-parallel-points(eu;a0;a1;b0;b1) ∧ geo-parallel-points(eu;a0;a1;c0;c1))
⇒ (Colinear(p;b0;b1) ∧ Colinear(p;c0;c1))
⇒ (Colinear(c0;b0;b1) ∧ Colinear(c1;b0;b1)))
Definitions occuring in Statement :
geo-parallel-points: geo-parallel-points(e;a;b;c;d),
geo-colinear: Colinear(a;b;c),
geo-point: Point,
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q
Definitions occuring in definition :
all: ∀x:A. B[x],
geo-point: Point,
geo-parallel-points: geo-parallel-points(e;a;b;c;d),
implies: P ⇒ Q,
and: P ∧ Q,
geo-colinear: Colinear(a;b;c)
FDL editor aliases :
PlayfairPP
Latex:
PlayfairPP(eu) ==
\mforall{}a0,a1,b0,b1,c0,c1,p:Point.
((geo-parallel-points(eu;a0;a1;b0;b1) \mwedge{} geo-parallel-points(eu;a0;a1;c0;c1))
{}\mRightarrow{} (Colinear(p;b0;b1) \mwedge{} Colinear(p;c0;c1))
{}\mRightarrow{} (Colinear(c0;b0;b1) \mwedge{} Colinear(c1;b0;b1)))
Date html generated:
2019_10_16-PM-01_47_55
Last ObjectModification:
2019_06_19-PM-01_47_33
Theory : euclidean!plane!geometry
Home
Index