Nuprl Definition : type-continuous
Continuous(T.F[T]) == ∀[X:ℕ ⟶ Type]. ((⋂n:ℕ. F[X n]) ⊆r F[⋂n:ℕ. (X n)])
Definitions occuring in Statement :
nat: ℕ,
subtype_rel: A ⊆r B,
uall: ∀[x:A]. B[x],
apply: f a,
isect: ⋂x:A. B[x],
function: x:A ⟶ B[x],
universe: Type
Definitions occuring in definition :
uall: ∀[x:A]. B[x],
function: x:A ⟶ B[x],
universe: Type,
subtype_rel: A ⊆r B,
isect: ⋂x:A. B[x],
nat: ℕ,
apply: f a
FDL editor aliases :
type-continuous
Latex:
Continuous(T.F[T]) == \mforall{}[X:\mBbbN{} {}\mrightarrow{} Type]. ((\mcap{}n:\mBbbN{}. F[X n]) \msubseteq{}r F[\mcap{}n:\mBbbN{}. (X n)])
Date html generated:
2016_05_13-PM-04_09_34
Last ObjectModification:
2015_09_22-PM-05_45_55
Theory : subtype_1
Home
Index