Nuprl Definition : eu-colinear-set
eu-colinear-set(e;L) == (∀A∈L.(∀B∈L.(∀C∈L.(¬(A = B ∈ Point)) ⇒ Colinear(A;B;C))))
Definitions occuring in Statement :
eu-colinear: Colinear(a;b;c),
eu-point: Point,
l_all: (∀x∈L.P[x]),
not: ¬A,
implies: P ⇒ Q,
equal: s = t ∈ T
Definitions occuring in definition :
l_all: (∀x∈L.P[x]),
implies: P ⇒ Q,
not: ¬A,
equal: s = t ∈ T,
eu-point: Point,
eu-colinear: Colinear(a;b;c)
FDL editor aliases :
eu-colinear-set
Latex:
eu-colinear-set(e;L) == (\mforall{}A\mmember{}L.(\mforall{}B\mmember{}L.(\mforall{}C\mmember{}L.(\mneg{}(A = B)) {}\mRightarrow{} Colinear(A;B;C))))
Date html generated:
2016_05_18-AM-06_40_15
Last ObjectModification:
2016_01_03-PM-01_51_10
Theory : euclidean!geometry
Home
Index