Nuprl Definition : incr-binary-seq
IBS == {s:ℕ ⟶ ℕ2| ∀i:ℕ. ((s i) ≤ (s (1 + i)))}
Definitions occuring in Statement :
int_seg: {i..j-},
nat: ℕ,
le: A ≤ B,
all: ∀x:A. B[x],
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
add: n + m,
natural_number: $n
Definitions occuring in definition :
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
int_seg: {i..j-},
all: ∀x:A. B[x],
nat: ℕ,
le: A ≤ B,
apply: f a,
add: n + m,
natural_number: $n
FDL editor aliases :
ibs
Latex:
IBS == \{s:\mBbbN{} {}\mrightarrow{} \mBbbN{}2| \mforall{}i:\mBbbN{}. ((s i) \mleq{} (s (1 + i)))\}
Date html generated:
2019_10_30-AM-10_15_38
Last ObjectModification:
2019_06_28-PM-01_55_32
Theory : real!vectors
Home
Index