Nuprl Definition : proj-line-sep
proj-line-sep(eu;l;m) ==
case l
of inl(l') =>
case m of inl(m') => geo-line-sep(eu;l';m') | inr(_) => True
| inr(_) =>
case m of inl(m') => True | inr(_) => False
Definitions occuring in Statement :
geo-line-sep: geo-line-sep(g;l;m),
false: False,
true: True,
decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions occuring in definition :
false: False,
true: True,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
geo-line-sep: geo-line-sep(g;l;m)
FDL editor aliases :
proj-line-sep
Latex:
proj-line-sep(eu;l;m) ==
case l
of inl(l') =>
case m of inl(m') => geo-line-sep(eu;l';m') | inr($_{}$) => True
| inr($_{}$) =>
case m of inl(m') => True | inr($_{}$) => False
Date html generated:
2018_05_22-PM-01_14_36
Last ObjectModification:
2018_05_21-PM-05_41_05
Theory : euclidean!plane!geometry
Home
Index