Nuprl Definition : rnonneg2
rnonneg2(x) == ∀n:ℕ+. ∃N:ℕ+. ∀m:{N...}. (((-2) * m) ≤ (n * (x m)))
Definitions occuring in Statement :
int_upper: {i...},
nat_plus: ℕ+,
le: A ≤ B,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
apply: f a,
multiply: n * m,
minus: -n,
natural_number: $n
Definitions occuring in definition :
exists: ∃x:A. B[x],
nat_plus: ℕ+,
all: ∀x:A. B[x],
int_upper: {i...},
le: A ≤ B,
minus: -n,
natural_number: $n,
multiply: n * m,
apply: f a
FDL editor aliases :
rnonneg2
Latex:
rnonneg2(x) == \mforall{}n:\mBbbN{}\msupplus{}. \mexists{}N:\mBbbN{}\msupplus{}. \mforall{}m:\{N...\}. (((-2) * m) \mleq{} (n * (x m)))
Date html generated:
2016_05_18-AM-07_01_23
Last ObjectModification:
2015_09_23-AM-09_01_12
Theory : reals
Home
Index