Nuprl Definition : real
ℝ == {f:ℕ+ ⟶ ℤ| regular-seq(f)}
Definitions occuring in Statement :
regular-int-seq: k-regular-seq(f),
nat_plus: ℕ+,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
natural_number: $n,
int: ℤ
Definitions occuring in definition :
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
nat_plus: ℕ+,
int: ℤ,
regular-int-seq: k-regular-seq(f),
natural_number: $n
FDL editor aliases :
real
real
Latex:
\mBbbR{} == \{f:\mBbbN{}\msupplus{} {}\mrightarrow{} \mBbbZ{}| regular-seq(f)\}
Date html generated:
2016_05_18-AM-06_46_48
Last ObjectModification:
2015_09_23-AM-09_00_36
Theory : reals
Home
Index