Nuprl Definition : frs-increasing
frs-increasing(p) == ∀i,j:ℕ||p||. (i < j ⇒ (p[i] < p[j]))
Definitions occuring in Statement :
rless: x < y,
select: L[n],
length: ||as||,
int_seg: {i..j-},
less_than: a < b,
all: ∀x:A. B[x],
implies: P ⇒ Q,
natural_number: $n
Definitions occuring in definition :
all: ∀x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
length: ||as||,
implies: P ⇒ Q,
less_than: a < b,
rless: x < y,
select: L[n]
FDL editor aliases :
frs-increasing
frs-increasing
Latex:
frs-increasing(p) == \mforall{}i,j:\mBbbN{}||p||. (i < j {}\mRightarrow{} (p[i] < p[j]))
Date html generated:
2016_05_18-AM-08_52_48
Last ObjectModification:
2015_09_23-AM-09_08_31
Theory : reals
Home
Index