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:  Q true: True apply: a function: x:A ⟶ B[x] natural_number: $n equal: t ∈ T
Definitions occuring in definition :  implies:  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: t ∈ T nat: apply: 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