Nuprl Definition : geo-tar-same-side

geo-tar-same-side(e;a;b;p;q) ==  ∃c:Point. (geo-tar-opp-side(e;a;c;p;q) ∧ geo-tar-opp-side(e;b;c;p;q))


Definitions occuring in Statement :  geo-tar-opp-side: geo-tar-opp-side(e;a;b;p;q),  geo-point: Point,  exists: ∃x:A. B[x],  and: P ∧ Q
Definitions occuring in definition :  exists: ∃x:A. B[x],  geo-point: Point,  and: P ∧ Q,  geo-tar-opp-side: geo-tar-opp-side(e;a;b;p;q)
FDL editor aliases :  geo-tar-same-side geo-tar-same-side
Latex:
geo-tar-same-side(e;a;b;p;q)  ==
    \mexists{}c:Point.  (geo-tar-opp-side(e;a;c;p;q)  \mwedge{}  geo-tar-opp-side(e;b;c;p;q))


Date html generated: 2017_10_02-PM-06_23_14
Last ObjectModification: 2017_08_05-PM-04_17_26

Theory : euclidean!plane!geometry


Home Index