Nuprl Definition : pseudo-bounded
pseudo-bounded(S) == ∀f:ℕ ⟶ S. ∃k:ℕ. ∀n:{k...}. f n < n
Definitions occuring in Statement :
int_upper: {i...},
nat: ℕ,
less_than: a < b,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
apply: f a,
function: x:A ⟶ B[x]
Definitions occuring in definition :
apply: f a,
less_than: a < b,
int_upper: {i...},
all: ∀x:A. B[x],
nat: ℕ,
exists: ∃x:A. B[x],
function: x:A ⟶ B[x]
FDL editor aliases :
pseudo-bounded
Latex:
pseudo-bounded(S) == \mforall{}f:\mBbbN{} {}\mrightarrow{} S. \mexists{}k:\mBbbN{}. \mforall{}n:\{k...\}. f n < n
Date html generated:
2016_12_12-AM-09_23_29
Last ObjectModification:
2016_11_22-PM-04_25_02
Theory : continuity
Home
Index