Nuprl Definition : bdd-diff
bdd-diff(f;g) == ∃B:ℕ. ∀n:ℕ+. (|(f n) - g n| ≤ B)
Definitions occuring in Statement :
absval: |i|,
nat_plus: ℕ+,
nat: ℕ,
le: A ≤ B,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
apply: f a,
subtract: n - m
Definitions occuring in definition :
exists: ∃x:A. B[x],
nat: ℕ,
all: ∀x:A. B[x],
nat_plus: ℕ+,
le: A ≤ B,
absval: |i|,
subtract: n - m,
apply: f a
FDL editor aliases :
bdd-diff
Latex:
bdd-diff(f;g) == \mexists{}B:\mBbbN{}. \mforall{}n:\mBbbN{}\msupplus{}. (|(f n) - g n| \mleq{} B)
Date html generated:
2016_05_18-AM-06_46_17
Last ObjectModification:
2015_09_23-AM-09_00_35
Theory : reals
Home
Index