Nuprl Definition : distinct-triangles
distinct-triangles(pg;t1;t2) ==
(fst(t1) ≠ fst(t2) ∧ fst(t1) ≠ fst(snd(t2)) ∧ fst(t1) ≠ fst(snd(snd(t2))))
∧ (fst(snd(t1)) ≠ fst(t2) ∧ fst(snd(t1)) ≠ fst(snd(t2)) ∧ fst(snd(t1)) ≠ fst(snd(snd(t2))))
∧ fst(snd(snd(t1))) ≠ fst(t2)
∧ fst(snd(snd(t1))) ≠ fst(snd(t2))
∧ fst(snd(snd(t1))) ≠ fst(snd(snd(t2)))
Definitions occuring in Statement :
pgeo-psep: a ≠ b,
pi1: fst(t),
pi2: snd(t),
and: P ∧ Q
Definitions occuring in definition :
and: P ∧ Q,
pgeo-psep: a ≠ b,
pi1: fst(t),
pi2: snd(t)
FDL editor aliases :
distinct-triangles
Latex:
distinct-triangles(pg;t1;t2) ==
(fst(t1) \mneq{} fst(t2) \mwedge{} fst(t1) \mneq{} fst(snd(t2)) \mwedge{} fst(t1) \mneq{} fst(snd(snd(t2))))
\mwedge{} (fst(snd(t1)) \mneq{} fst(t2) \mwedge{} fst(snd(t1)) \mneq{} fst(snd(t2)) \mwedge{} fst(snd(t1)) \mneq{} fst(snd(snd(t2))))
\mwedge{} fst(snd(snd(t1))) \mneq{} fst(t2)
\mwedge{} fst(snd(snd(t1))) \mneq{} fst(snd(t2))
\mwedge{} fst(snd(snd(t1))) \mneq{} fst(snd(snd(t2)))
Date html generated:
2018_05_22-PM-00_48_42
Last ObjectModification:
2017_12_05-PM-01_54_29
Theory : euclidean!plane!geometry
Home
Index