Nuprl Definition : nondecreasing
nondecreasing(f;k) ==  ∀i:ℕk - 1. ((f i) ≤ (f (i + 1)))
Definitions occuring in Statement : 
int_seg: {i..j-}
, 
le: A ≤ B
, 
all: ∀x:A. B[x]
, 
apply: f a
, 
subtract: n - m
, 
add: n + m
, 
natural_number: $n
Definitions occuring in definition : 
all: ∀x:A. B[x]
, 
int_seg: {i..j-}
, 
subtract: n - m
, 
le: A ≤ B
, 
apply: f a
, 
add: n + m
, 
natural_number: $n
FDL editor aliases : 
nondecreasing
Latex:
nondecreasing(f;k)  ==    \mforall{}i:\mBbbN{}k  -  1.  ((f  i)  \mleq{}  (f  (i  +  1)))
Date html generated:
2016_05_14-PM-09_29_47
Last ObjectModification:
2015_09_22-PM-06_03_12
Theory : num_thy_1
Home
Index