Nuprl Definition : irrational
irrational(x) == ∀a:ℤ. ∀b:ℕ+. x ≠ (r(a)/r(b))
Definitions occuring in Statement :
rdiv: (x/y),
rneq: x ≠ y,
int-to-real: r(n),
nat_plus: ℕ+,
all: ∀x:A. B[x],
int: ℤ
Definitions occuring in definition :
int: ℤ,
all: ∀x:A. B[x],
nat_plus: ℕ+,
rneq: x ≠ y,
rdiv: (x/y),
int-to-real: r(n)
FDL editor aliases :
irrational
irrational
Latex:
irrational(x) == \mforall{}a:\mBbbZ{}. \mforall{}b:\mBbbN{}\msupplus{}. x \mneq{} (r(a)/r(b))
Date html generated:
2016_05_18-AM-09_51_03
Last ObjectModification:
2016_02_01-PM-03_00_24
Theory : reals
Home
Index