Nuprl Definition : i-member
r ∈ I ==
let l,u = I
in case l
of inl(x) =>
case x
of inl(a) =>
case u of inl(y) => case y of inl(b) => (a ≤ r) ∧ (r ≤ b) | inr(b) => (a ≤ r) ∧ (r < b) | inr(y) => a ≤ r
| inr(a) =>
case u of inl(y) => case y of inl(b) => (a < r) ∧ (r ≤ b) | inr(b) => (a < r) ∧ (r < b) | inr(y) => a < r
| inr(x) =>
case u of inl(y) => case y of inl(b) => r ≤ b | inr(b) => r < b | inr(y) => True
Definitions occuring in Statement :
rleq: x ≤ y,
rless: x < y,
and: P ∧ Q,
true: True,
spread: spread def,
decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions occuring in definition :
spread: spread def,
and: P ∧ Q,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
rleq: x ≤ y,
rless: x < y,
true: True
FDL editor aliases :
i-member
i-member
Latex:
r \mmember{} I ==
let l,u = I
in case l
of inl(x) =>
case x
of inl(a) =>
case u
of inl(y) =>
case y of inl(b) => (a \mleq{} r) \mwedge{} (r \mleq{} b) | inr(b) => (a \mleq{} r) \mwedge{} (r < b)
| inr(y) =>
a \mleq{} r
| inr(a) =>
case u
of inl(y) =>
case y of inl(b) => (a < r) \mwedge{} (r \mleq{} b) | inr(b) => (a < r) \mwedge{} (r < b)
| inr(y) =>
a < r
| inr(x) =>
case u of inl(y) => case y of inl(b) => r \mleq{} b | inr(b) => r < b | inr(y) => True
Date html generated:
2016_05_18-AM-08_19_05
Last ObjectModification:
2015_09_23-AM-09_05_50
Theory : reals
Home
Index