Nuprl Definition : line-triangle
LΔ(l;m;n) == ∀l,m,n:Line. ∀s:m ≠ n. m ∧ n ≠ l
Definitions occuring in Statement :
pgeo-meet: l ∧ m
,
pgeo-lsep: l ≠ m
,
pgeo-plsep: a ≠ b
,
pgeo-line: Line
,
all: ∀x:A. B[x]
Definitions occuring in definition :
pgeo-line: Line
,
all: ∀x:A. B[x]
,
pgeo-lsep: l ≠ m
,
pgeo-plsep: a ≠ b
,
pgeo-meet: l ∧ m
FDL editor aliases :
l-tri
Latex:
L\mDelta{}(l;m;n) == \mforall{}l,m,n:Line. \mforall{}s:m \mneq{} n. m \mwedge{} n \mneq{} l
Date html generated:
2018_05_22-PM-00_49_30
Last ObjectModification:
2017_12_01-AM-09_50_35
Theory : euclidean!plane!geometry
Home
Index