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