Nuprl Definition : seq-cont
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 :
quotient: x,y:A//B[x; y],
int_upper: {i...},
int_seg: {i..j-},
nat: ℕ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
true: True,
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,
quotient: x,y:A//B[x; y],
exists: ∃x:A. B[x],
all: ∀x:A. B[x],
int_upper: {i...},
equal: s = t ∈ T,
nat: ℕ,
apply: f a,
true: True
FDL editor aliases :
seq-cont
Latex:
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{} \00D9(\mexists{}n:\mBbbN{}. \mforall{}m:\{n...\}. ((F (g m)) = (F f))))
Date html generated:
2017_09_29-PM-06_05_44
Last ObjectModification:
2017_07_19-AM-10_36_00
Theory : continuity
Home
Index