Nuprl Definition : Post5
Post5(e) ==
∀a,b,c,d,x,y:Point.
(((Colinear(x;a;b) ∧ Colinear(y;c;d)) ∧ a leftof yx ∧ c leftof yx ∧ (∀i,j,k:Point. (axy + cyx ≅ ijk ∧ i # jk)))
⇒ ab \/ cd)
Definitions occuring in Statement :
hp-angle-sum: abc + xyz ≅ def,
geo-intersect-points: ab \/ cd,
geo-lsep: a # bc,
geo-colinear: Colinear(a;b;c),
geo-left: a leftof bc,
geo-point: Point,
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q
Definitions occuring in definition :
implies: P ⇒ Q,
geo-colinear: Colinear(a;b;c),
geo-left: a leftof bc,
all: ∀x:A. B[x],
geo-point: Point,
and: P ∧ Q,
hp-angle-sum: abc + xyz ≅ def,
geo-lsep: a # bc,
geo-intersect-points: ab \/ cd
FDL editor aliases :
Post5
Latex:
Post5(e) ==
\mforall{}a,b,c,d,x,y:Point.
(((Colinear(x;a;b) \mwedge{} Colinear(y;c;d))
\mwedge{} a leftof yx
\mwedge{} c leftof yx
\mwedge{} (\mforall{}i,j,k:Point. (axy + cyx \mcong{} ijk \mwedge{} i \# jk)))
{}\mRightarrow{} ab \mbackslash{}/ cd)
Date html generated:
2019_10_16-PM-02_36_55
Last ObjectModification:
2019_06_19-PM-02_37_51
Theory : euclidean!plane!geometry
Home
Index