### Nuprl Definition : basic-strong-continuity

`basic-strong-continuity(T;F) ==`
`  ∃M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ ⋃ (ℕ × ℕ)) [(∀f:ℕ ⟶ T`
`                                           ((∃n:ℕ. ((M n f) = (F f) ∈ ℕ))`
`                                           ∧ (∀n:ℕ. (M n f) = (F f) ∈ ℕ supposing M n f is an integer)`
`                                           ∧ (∀n,m:ℕ.  ((n ≤ m) `` M n f is an integer `` M m f is an integer))))]`

Definitions occuring in Statement :  int_seg: `{i..j-}` nat: `ℕ` b-union: `A ⋃ B` uimplies: `b supposing a` isint: isint def le: `A ≤ B` all: `∀x:A. B[x]` sq_exists: `∃x:A [B[x]]` exists: `∃x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` false: `False` true: `True` apply: `f a` function: `x:A ⟶ B[x]` product: `x:A × B[x]` natural_number: `\$n` equal: `s = t ∈ T`
Definitions occuring in definition :  sq_exists: `∃x:A [B[x]]` int_seg: `{i..j-}` natural_number: `\$n` b-union: `A ⋃ B` product: `x:A × B[x]` function: `x:A ⟶ B[x]` exists: `∃x:A. B[x]` and: `P ∧ Q` uimplies: `b supposing a` equal: `s = t ∈ T` all: `∀x:A. B[x]` nat: `ℕ` le: `A ≤ B` implies: `P `` Q` isint: isint def apply: `f a` true: `True` false: `False`
FDL editor aliases :  basic-strong-continuity

Latex:
basic-strong-continuity(T;F)  ==
\mexists{}M:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  (\mBbbN{}  \mcup{}  (\mBbbN{}  \mtimes{}  \mBbbN{}))  [(\mforall{}f:\mBbbN{}  {}\mrightarrow{}  T
((\mexists{}n:\mBbbN{}.  ((M  n  f)  =  (F  f)))
\mwedge{}  (\mforall{}n:\mBbbN{}.  (M  n  f)  =  (F  f)  supposing  M  n  f  is  an  integer)
\mwedge{}  (\mforall{}n,m:\mBbbN{}.
((n  \mleq{}  m)
{}\mRightarrow{}  M  n  f  is  an  integer
{}\mRightarrow{}  M  m  f  is  an  integer))))]

Date html generated: 2019_06_20-PM-02_50_11
Last ObjectModification: 2019_02_11-AM-11_18_07

Theory : continuity

Home Index