Nuprl Definition : strict-inc
StrictInc == {s:ℕ ⟶ ℕ| ∀j:ℕ. ∀i:ℕj. s i < s j}
Definitions occuring in Statement :
int_seg: {i..j-},
nat: ℕ,
less_than: a < b,
all: ∀x:A. B[x],
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n
Definitions occuring in definition :
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
nat: ℕ,
all: ∀x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
less_than: a < b,
apply: f a
FDL editor aliases :
strict-inc
Latex:
StrictInc == \{s:\mBbbN{} {}\mrightarrow{} \mBbbN{}| \mforall{}j:\mBbbN{}. \mforall{}i:\mBbbN{}j. s i < s j\}
Date html generated:
2016_05_14-PM-09_47_16
Last ObjectModification:
2015_12_18-AM-11_05_03
Theory : continuity
Home
Index