Nuprl Definition : req

x = y == ∀n:ℕ⁺. (|(x n) - y n| ≤ 4)

Definitions occuring in Statement : absval: |i|, nat_plus: ℕ⁺, le: A ≤ B, all: ∀x:A. B[x], apply: f a, subtract: n - m, natural_number: $n
Definitions occuring in definition : all: ∀x:A. B[x], nat_plus: ℕ⁺, le: A ≤ B, absval: |i|, subtract: n - m, apply: f a, natural_number: $n
FDL editor aliases : req req

Latex:
x = y == \mforall{}n:\mBbbN{}\msupplus{}. (|(x n) - y n| \mleq{} 4) Date html generated: 2016_05_18-AM-06_50_13 Last ObjectModification: 2015_09_23-AM-09_00_45 Theory : reals Home Index