Nuprl Definition : type-incr-chain
type-incr-chain{i:l}() ==  {X:ℕ ⟶ Type| ∀n:ℕ. ((X n) ⊆r (X (n + 1)))} 
Definitions occuring in Statement : 
nat: ℕ
, 
subtype_rel: A ⊆r B
, 
all: ∀x:A. B[x]
, 
set: {x:A| B[x]} 
, 
apply: f a
, 
function: x:A ⟶ B[x]
, 
add: n + 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 ⊆r B
, 
apply: f a
, 
add: n + 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