Nuprl Definition : k-continuous

k-Continuous(T.F[T]) ==  ∀[X:ℕ ⟶ ℕk ⟶ Type]. ((∀n:ℕ(n 1) ⊆ n)  ⋂n. F[X n] ⊆ F[⋂n. n])



Definitions occuring in Statement :  k-intersection: n. X[n] k-subtype: A ⊆ B int_seg: {i..j-} nat: uall: [x:A]. B[x] all: x:A. B[x] implies:  Q apply: a function: x:A ⟶ B[x] add: m natural_number: $n universe: Type
Definitions occuring in definition :  uall: [x:A]. B[x] function: x:A ⟶ B[x] int_seg: {i..j-} universe: Type implies:  Q all: x:A. B[x] nat: add: m natural_number: $n k-subtype: A ⊆ B k-intersection: n. X[n] apply: a
FDL editor aliases :  k-continuous

Latex:
k-Continuous(T.F[T])  ==    \mforall{}[X:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}k  {}\mrightarrow{}  Type].  ((\mforall{}n:\mBbbN{}.  X  (n  +  1)  \msubseteq{}  X  n)  {}\mRightarrow{}  \mcap{}n.  F[X  n]  \msubseteq{}  F[\mcap{}n.  X  n])



Date html generated: 2018_05_21-PM-00_09_31
Last ObjectModification: 2017_10_18-PM-02_34_42

Theory : co-recursion


Home Index