Nuprl Definition : line-sep-from-point-triangle
l ≠ PΔ(a;b;c) == ∀l:Line. ∀a,b,c:Point. (((a ≠ l ∧ b ≠ l) ∧ c ≠ l) ∧ PΔ(a;b;c))
Definitions occuring in Statement :
point-triangle: PΔ(a;b;c),
pgeo-plsep: a ≠ b,
pgeo-line: Line,
pgeo-point: Point,
all: ∀x:A. B[x],
and: P ∧ Q
Definitions occuring in definition :
pgeo-line: Line,
all: ∀x:A. B[x],
pgeo-point: Point,
and: P ∧ Q,
pgeo-plsep: a ≠ b,
point-triangle: PΔ(a;b;c)
FDL editor aliases :
l-sep-ptri
Latex:
l \mneq{} P\mDelta{}(a;b;c) == \mforall{}l:Line. \mforall{}a,b,c:Point. (((a \mneq{} l \mwedge{} b \mneq{} l) \mwedge{} c \mneq{} l) \mwedge{} P\mDelta{}(a;b;c))
Date html generated:
2018_05_22-PM-00_50_13
Last ObjectModification:
2017_12_01-PM-03_08_36
Theory : euclidean!plane!geometry
Home
Index