Nuprl Definition : q-rel
q-rel(r;x) == if (r =z 0) then 0 = x ∈ ℚ if (r =z 1) then 0 ≤ x else 0 < x fi
Definitions occuring in Statement :
qle: r ≤ s,
qless: r < s,
rationals: ℚ,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
natural_number: $n,
equal: s = t ∈ T
Definitions occuring in definition :
equal: s = t ∈ T,
rationals: ℚ,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
qle: r ≤ s,
qless: r < s,
natural_number: $n
FDL editor aliases :
q-rel
Latex:
q-rel(r;x) == if (r =\msubz{} 0) then 0 = x if (r =\msubz{} 1) then 0 \mleq{} x else 0 < x fi
Date html generated:
2016_05_15-PM-11_17_40
Last ObjectModification:
2015_09_23-AM-08_28_12
Theory : rationals
Home
Index