Nuprl Definition : sorted
sorted(L) == ∀i:ℕ||L||. ∀j:ℕi. (L[j] ≤ L[i])
Definitions occuring in Statement :
select: L[n],
length: ||as||,
int_seg: {i..j-},
le: A ≤ B,
all: ∀x:A. B[x],
natural_number: $n
Definitions occuring in definition :
length: ||as||,
all: ∀x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
le: A ≤ B,
select: L[n]
FDL editor aliases :
sorted
Latex:
sorted(L) == \mforall{}i:\mBbbN{}||L||. \mforall{}j:\mBbbN{}i. (L[j] \mleq{} L[i])
Date html generated:
2016_05_14-AM-06_36_08
Last ObjectModification:
2015_12_03-PM-02_07_07
Theory : list_0
Home
Index