Nuprl Definition : strong-type-continuous
Continuous+(T.F[T]) == ∀[X:ℕ ⟶ Type]. ⋂n:ℕ. F[X n] ≡ F[⋂n:ℕ. (X n)]
Definitions occuring in Statement :
nat: ℕ,
ext-eq: A ≡ 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,
ext-eq: A ≡ B,
isect: ⋂x:A. B[x],
nat: ℕ,
apply: f a
FDL editor aliases :
strong-type-continuous
Latex:
Continuous+(T.F[T]) == \mforall{}[X:\mBbbN{} {}\mrightarrow{} Type]. \mcap{}n:\mBbbN{}. F[X n] \mequiv{} F[\mcap{}n:\mBbbN{}. (X n)]
Date html generated:
2016_05_13-PM-04_09_36
Last ObjectModification:
2015_09_22-PM-05_45_55
Theory : subtype_1
Home
Index