Nuprl Definition : is-infinitesmal
is-infinitesmal(x) == ∀n:ℕ+. |x| < ((r1/r(n)))*
Definitions occuring in Statement :
rstar: (x)*,
rless*: x < y,
rabs*: |x|,
rdiv: (x/y),
int-to-real: r(n),
nat_plus: ℕ+,
all: ∀x:A. B[x],
natural_number: $n
Definitions occuring in definition :
all: ∀x:A. B[x],
nat_plus: ℕ+,
rless*: x < y,
rabs*: |x|,
rstar: (x)*,
rdiv: (x/y),
natural_number: $n,
int-to-real: r(n)
FDL editor aliases :
is-infinitesmal
Latex:
is-infinitesmal(x) == \mforall{}n:\mBbbN{}\msupplus{}. |x| < ((r1/r(n)))*
Date html generated:
2018_05_22-PM-09_28_46
Last ObjectModification:
2017_10_06-PM-03_58_53
Theory : reals_2
Home
Index