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