Nuprl Definition : descending
descending(a,b.<[a; b];L) == ∀i:ℕ||L|| - 1. <[L[i + 1]; L[i]]
Definitions occuring in Statement :
select: L[n],
length: ||as||,
int_seg: {i..j-},
all: ∀x:A. B[x],
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,
length: ||as||,
add: n + m,
natural_number: $n,
select: L[n]
FDL editor aliases :
descending
Latex:
descending(a,b.<[a; b];L) == \mforall{}i:\mBbbN{}||L|| - 1. <[L[i + 1]; L[i]]
Date html generated:
2016_05_15-PM-04_16_27
Last ObjectModification:
2015_09_23-AM-07_47_39
Theory : general
Home
Index