Nuprl Definition : sorted-seq
sorted-seq(x,y.R[x; y];s) == ∀i,j:ℕ||s||. (i < j ⇒ R[s[i]; s[j]])
Definitions occuring in Statement :
seq-item: s[i],
seq-len: ||s||,
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,
seq-len: ||s||,
implies: P ⇒ Q,
less_than: a < b,
seq-item: s[i]
FDL editor aliases :
sorted-seq
Latex:
sorted-seq(x,y.R[x; y];s) == \mforall{}i,j:\mBbbN{}||s||. (i < j {}\mRightarrow{} R[s[i]; s[j]])
Date html generated:
2019_06_20-AM-11_26_50
Last ObjectModification:
2019_01_15-AM-11_09_32
Theory : arithmetic
Home
Index