Nuprl Definition : strictly-increasing-seq
strictly-increasing-seq(n;s) == ∀j:ℕn. ∀i:ℕj. s i < s j
Definitions occuring in Statement :
int_seg: {i..j-},
less_than: a < b,
all: ∀x:A. B[x],
apply: f a,
natural_number: $n
Definitions occuring in definition :
all: ∀x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
less_than: a < b,
apply: f a
FDL editor aliases :
strictly-increasing-seq
Latex:
strictly-increasing-seq(n;s) == \mforall{}j:\mBbbN{}n. \mforall{}i:\mBbbN{}j. s i < s j
Date html generated:
2016_05_13-PM-03_48_29
Last ObjectModification:
2015_09_22-PM-05_45_18
Theory : bar-induction
Home
Index