Nuprl Definition : non-rational
non-rational() == {x:ℝ| ∀a:ℤ. ∀b:ℕ+. (¬(x = (r(a)/r(b))))}
Definitions occuring in Statement :
rdiv: (x/y),
req: x = y,
int-to-real: r(n),
real: ℝ,
nat_plus: ℕ+,
all: ∀x:A. B[x],
not: ¬A,
set: {x:A| B[x]} ,
int: ℤ
Definitions occuring in definition :
set: {x:A| B[x]} ,
real: ℝ,
int: ℤ,
all: ∀x:A. B[x],
nat_plus: ℕ+,
not: ¬A,
req: x = y,
rdiv: (x/y),
int-to-real: r(n)
FDL editor aliases :
non-rational
Latex:
non-rational() == \{x:\mBbbR{}| \mforall{}a:\mBbbZ{}. \mforall{}b:\mBbbN{}\msupplus{}. (\mneg{}(x = (r(a)/r(b))))\}
Date html generated:
2017_10_03-AM-10_18_08
Last ObjectModification:
2017_07_10-AM-10_36_56
Theory : reals
Home
Index