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