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