Nuprl Definition : type-incr-chain

type-incr-chain{i:l}() ==  {X:ℕ ⟶ Type| ∀n:ℕ((X n) ⊆(X (n 1)))} 



Definitions occuring in Statement :  nat: subtype_rel: A ⊆B all: x:A. B[x] set: {x:A| B[x]}  apply: a function: x:A ⟶ B[x] add: m natural_number: $n universe: Type
Definitions occuring in definition :  set: {x:A| B[x]}  function: x:A ⟶ B[x] universe: Type all: x:A. B[x] nat: subtype_rel: A ⊆B apply: a add: m natural_number: $n
FDL editor aliases :  type-incr-chain

Latex:
type-incr-chain\{i:l\}()  ==    \{X:\mBbbN{}  {}\mrightarrow{}  Type|  \mforall{}n:\mBbbN{}.  ((X  n)  \msubseteq{}r  (X  (n  +  1)))\} 



Date html generated: 2016_05_15-PM-06_51_20
Last ObjectModification: 2015_09_23-AM-08_07_00

Theory : general


Home Index