Nuprl Definition : r-rational
r-rational(x) == ∃a:ℤ. ∃b:ℕ+. (x = (r(a)/r(b)))
Definitions occuring in Statement :
rdiv: (x/y),
req: x = y,
int-to-real: r(n),
nat_plus: ℕ+,
exists: ∃x:A. B[x],
int: ℤ
Definitions occuring in definition :
int: ℤ,
exists: ∃x:A. B[x],
nat_plus: ℕ+,
req: x = y,
rdiv: (x/y),
int-to-real: r(n)
FDL editor aliases :
r-rational
Latex:
r-rational(x) == \mexists{}a:\mBbbZ{}. \mexists{}b:\mBbbN{}\msupplus{}. (x = (r(a)/r(b)))
Date html generated:
2016_05_18-AM-09_50_41
Last ObjectModification:
2015_09_23-AM-09_13_35
Theory : reals
Home
Index