Nuprl Definition : frs-non-dec
frs-non-dec(L) == ∀i,j:ℕ||L||. ((i ≤ j) ⇒ (L[i] ≤ L[j]))
Definitions occuring in Statement :
rleq: x ≤ y,
select: L[n],
length: ||as||,
int_seg: {i..j-},
le: 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,
le: A ≤ B,
rleq: x ≤ y,
select: L[n]
FDL editor aliases :
frs-non-dec
frs-non-dec
Latex:
frs-non-dec(L) == \mforall{}i,j:\mBbbN{}||L||. ((i \mleq{} j) {}\mRightarrow{} (L[i] \mleq{} L[j]))
Date html generated:
2016_05_18-AM-08_51_38
Last ObjectModification:
2015_09_23-AM-09_08_18
Theory : reals
Home
Index