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