Nuprl Definition : geo-tar-opp-side
geo-tar-opp-side(e;a;b;p;q) == (a # pq ∧ b # pq) ∧ (∃t:Point. (Colinear(p;q;t) ∧ a_t_b))
Definitions occuring in Statement :
geo-lsep: a # bc,
geo-colinear: Colinear(a;b;c),
geo-between: a_b_c,
geo-point: Point,
exists: ∃x:A. B[x],
and: P ∧ Q
Definitions occuring in definition :
geo-lsep: a # bc,
exists: ∃x:A. B[x],
geo-point: Point,
and: P ∧ Q,
geo-colinear: Colinear(a;b;c),
geo-between: a_b_c
FDL editor aliases :
geo-tar-opp-side
geo-tar-opp-side
Latex:
geo-tar-opp-side(e;a;b;p;q) == (a \# pq \mwedge{} b \# pq) \mwedge{} (\mexists{}t:Point. (Colinear(p;q;t) \mwedge{} a\_t\_b))
Date html generated:
2017_10_02-PM-06_23_04
Last ObjectModification:
2017_08_10-PM-03_40_22
Theory : euclidean!plane!geometry
Home
Index