Nuprl Definition : unsquashed-seq-cont
unsquashed-seq-cont(T;F) ==
∀f:ℕ ⟶ T. ∀g:ℕ ⟶ ℕ ⟶ T.
((∀k:ℕ. ∃n:ℕ. ∀m:{n...}. ((g m) = f ∈ (ℕk ⟶ T))) ⇒ (∃n:ℕ. ∀m:{n...}. ((F (g m)) = (F f) ∈ ℕ)))
Definitions occuring in Statement :
int_upper: {i...},
int_seg: {i..j-},
nat: ℕ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n,
equal: s = t ∈ T
Definitions occuring in definition :
implies: P ⇒ Q,
function: x:A ⟶ B[x],
int_seg: {i..j-},
natural_number: $n,
exists: ∃x:A. B[x],
all: ∀x:A. B[x],
int_upper: {i...},
equal: s = t ∈ T,
nat: ℕ,
apply: f a
FDL editor aliases :
unsquashed-seq-cont
Latex:
unsquashed-seq-cont(T;F) ==
\mforall{}f:\mBbbN{} {}\mrightarrow{} T. \mforall{}g:\mBbbN{} {}\mrightarrow{} \mBbbN{} {}\mrightarrow{} T.
((\mforall{}k:\mBbbN{}. \mexists{}n:\mBbbN{}. \mforall{}m:\{n...\}. ((g m) = f)) {}\mRightarrow{} (\mexists{}n:\mBbbN{}. \mforall{}m:\{n...\}. ((F (g m)) = (F f))))
Date html generated:
2017_09_29-PM-06_05_50
Last ObjectModification:
2017_07_19-AM-11_25_48
Theory : continuity
Home
Index