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