Nuprl Definition : proj-point-sep

proj-point-sep(eu;p;q) ==
  case p
   of inl(p') =>
   case q of inl(q') => p' ≠ q' | inr(q') => True
   | inr(p') =>
   case q of inl(q') => True | inr(q') => p' \/ q'

Definitions occuring in Statement : geo-intersect: L \/ M, geo-sep: a ≠ b, true: True, decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions occuring in definition : geo-intersect: L \/ M, true: True, decide: case b of inl(x) => s[x] | inr(y) => t[y], geo-sep: a ≠ b
FDL editor aliases : proj-point-sep

Latex:
proj-point-sep(eu;p;q) == case p of inl(p') => case q of inl(q') => p' \mneq{} q' | inr(q') => True | inr(p') => case q of inl(q') => True | inr(q') => p' \mbackslash{}/ q' Date html generated: 2018_05_22-PM-01_13_18 Last ObjectModification: 2018_05_19-AM-10_16_14 Theory : euclidean!plane!geometry Home Index