Nuprl Definition : pgeo-triangle
pgeo-triangle(pg) == a:Point × b:Point × c:Point × s:b ≠ c × a ≠ b ∨ c
Definitions occuring in Statement :
pgeo-join: p ∨ q,
pgeo-psep: a ≠ b,
pgeo-plsep: a ≠ b,
pgeo-point: Point,
product: x:A × B[x]
Definitions occuring in definition :
pgeo-point: Point,
product: x:A × B[x],
pgeo-psep: a ≠ b,
pgeo-plsep: a ≠ b,
pgeo-join: p ∨ q
FDL editor aliases :
pgeo-triangle
Latex:
pgeo-triangle(pg) == a:Point \mtimes{} b:Point \mtimes{} c:Point \mtimes{} s:b \mneq{} c \mtimes{} a \mneq{} b \mvee{} c
Date html generated:
2018_05_22-PM-00_50_57
Last ObjectModification:
2017_12_01-PM-04_35_14
Theory : euclidean!plane!geometry
Home
Index