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