Nuprl Definition : pp-sep
pp-sep(eu;p;l) ==
case p
of inl(p') =>
case l of inl(l') => p' # l' | inr(_) => True
| inr(p') =>
case l of inl(l') => p' \/ l' | inr(_) => False
Definitions occuring in Statement :
geo-plsep: p # l,
geo-intersect: L \/ M,
false: False,
true: True,
decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions occuring in definition :
false: False,
geo-intersect: L \/ M,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
true: True,
geo-plsep: p # l
FDL editor aliases :
pp-sep
Latex:
pp-sep(eu;p;l) ==
case p
of inl(p') =>
case l of inl(l') => p' \# l' | inr($_{}$) => True
| inr(p') =>
case l of inl(l') => p' \mbackslash{}/ l' | inr($_{}$) => False
Date html generated:
2018_05_22-PM-01_12_56
Last ObjectModification:
2018_05_19-AM-10_13_55
Theory : euclidean!plane!geometry
Home
Index