Nuprl Definition : geo-incident
p I L ==  ∀l:Line. ((l = L ∈ LINE) 
⇒ Colinear(p;fst(l);fst(snd(l))))
Definitions occuring in Statement : 
geoline: LINE
, 
geo-line: Line
, 
geo-colinear: Colinear(a;b;c)
, 
pi1: fst(t)
, 
pi2: snd(t)
, 
all: ∀x:A. B[x]
, 
implies: P 
⇒ Q
, 
equal: s = t ∈ T
Definitions occuring in definition : 
pi2: snd(t)
, 
pi1: fst(t)
, 
geo-colinear: Colinear(a;b;c)
, 
geoline: LINE
, 
equal: s = t ∈ T
, 
implies: P 
⇒ Q
, 
geo-line: Line
, 
all: ∀x:A. B[x]
FDL editor aliases : 
geo-incident
Latex:
p  I  L  ==    \mforall{}l:Line.  ((l  =  L)  {}\mRightarrow{}  Colinear(p;fst(l);fst(snd(l))))
Date html generated:
2018_05_22-PM-01_03_20
Last ObjectModification:
2018_05_10-PM-04_34_59
Theory : euclidean!plane!geometry
Home
Index