Nuprl Definition : geo-line-sep
geo-line-sep(g;l;m) ==  ∃p:Point. (Colinear(p;fst(l);fst(snd(l))) ∧ p # fst(m)fst(snd(m)))
Definitions occuring in Statement : 
geo-lsep: a # bc
, 
geo-colinear: Colinear(a;b;c)
, 
geo-point: Point
, 
pi1: fst(t)
, 
pi2: snd(t)
, 
exists: ∃x:A. B[x]
, 
and: P ∧ Q
Definitions occuring in definition : 
exists: ∃x:A. B[x]
, 
geo-point: Point
, 
and: P ∧ Q
, 
geo-colinear: Colinear(a;b;c)
, 
geo-lsep: a # bc
, 
pi1: fst(t)
, 
pi2: snd(t)
FDL editor aliases : 
geo-line-sep
Latex:
geo-line-sep(g;l;m)  ==    \mexists{}p:Point.  (Colinear(p;fst(l);fst(snd(l)))  \mwedge{}  p  \#  fst(m)fst(snd(m)))
Date html generated:
2018_05_22-PM-01_00_03
Last ObjectModification:
2018_01_16-AM-10_12_28
Theory : euclidean!plane!geometry
Home
Index