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
FDL editor aliases :
ibs
Latex:
IBS == \{s:\mBbbN{} {}\mrightarrow{} \mBbbN{}2| \mforall{}i:\mBbbN{}. ((s i) \mleq{} (s (1 + i)))\}
Date html generated:
2020_05_20-PM-00_03_20
Last ObjectModification:
2019_12_13-PM-02_38_13
Theory : reals
Home
Index