Nuprl Definition : geo-sep-line
geo-sep-line(e;a;b;c) == ∀z:Point. (Colinear(z;b;c) ⇒ a ≠ z)
Definitions occuring in Statement :
geo-colinear: Colinear(a;b;c),
geo-sep: a ≠ b,
geo-point: Point,
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions occuring in definition :
all: ∀x:A. B[x],
geo-point: Point,
implies: P ⇒ Q,
geo-colinear: Colinear(a;b;c),
geo-sep: a ≠ b
FDL editor aliases :
geo-sep-line
geo-sep-line
Latex:
geo-sep-line(e;a;b;c) == \mforall{}z:Point. (Colinear(z;b;c) {}\mRightarrow{} a \mneq{} z)
Date html generated:
2017_10_02-PM-06_22_24
Last ObjectModification:
2017_08_05-PM-04_16_43
Theory : euclidean!plane!geometry
Home
Index