Nuprl Definition : strong-regular-int-seq
strong-regular-int-seq(a;b;f) == ∀n,m:ℕ+. ((a * |(m * (f n)) - n * (f m)|) ≤ (b * (n + m)))
Definitions occuring in Statement :
absval: |i|,
nat_plus: ℕ+,
le: A ≤ B,
all: ∀x:A. B[x],
apply: f a,
multiply: n * m,
subtract: n - m,
add: n + m
Definitions occuring in definition :
add: n + m,
multiply: n * m,
apply: f a,
subtract: n - m,
absval: |i|,
le: A ≤ B,
nat_plus: ℕ+,
all: ∀x:A. B[x]
FDL editor aliases :
strong-regular-int-seq
Latex:
strong-regular-int-seq(a;b;f) == \mforall{}n,m:\mBbbN{}\msupplus{}. ((a * |(m * (f n)) - n * (f m)|) \mleq{} (b * (n + m)))
Date html generated:
2017_10_02-PM-07_12_52
Last ObjectModification:
2017_09_20-PM-04_56_01
Theory : reals
Home
Index