Nuprl Definition : rleq2
rleq2(x;y) == ∀n:ℕ+. ∃N:ℕ+. ∀m:{N...}. (((-2) * m) ≤ (n * ((y m) - 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,
subtract: 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,
subtract: n - m,
apply: f a
FDL editor aliases :
rleq2
Latex:
rleq2(x;y) == \mforall{}n:\mBbbN{}\msupplus{}. \mexists{}N:\mBbbN{}\msupplus{}. \mforall{}m:\{N...\}. (((-2) * m) \mleq{} (n * ((y m) - x m)))
Date html generated:
2016_05_18-AM-07_15_04
Last ObjectModification:
2015_09_23-AM-09_01_32
Theory : reals
Home
Index