Nuprl Definition : endpoints
endpoints(I) == let l,u = I in <case outl(l) of inl(a) => a | inr(a) => a, case outl(u) of inl(b) => b | inr(b) => b>
Definitions occuring in Statement :
outl: outl(x),
spread: spread def,
pair: <a, b>,
decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions occuring in definition :
spread: spread def,
pair: <a, b>,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
outl: outl(x)
FDL editor aliases :
endpoints
endpoints
Latex:
endpoints(I) ==
let l,u = I
in <case outl(l) of inl(a) => a | inr(a) => a, case outl(u) of inl(b) => b | inr(b) => b>
Date html generated:
2016_05_18-AM-08_17_18
Last ObjectModification:
2015_09_23-AM-09_05_16
Theory : reals
Home
Index