Nuprl Definition : type-family-continuous
type-family-continuous{i:l}(P;H) == ∀[X:ℕ ⟶ P ⟶ Type]. ⋂n:ℕ. H (X n) ⊆ H ⋂n:ℕ. X n
Definitions occuring in Statement :
sub-family: F ⊆ G,
isect-family: ⋂a:A. F[a],
nat: ℕ,
uall: ∀[x:A]. B[x],
apply: f a,
function: x:A ⟶ B[x],
universe: Type
Definitions occuring in definition :
uall: ∀[x:A]. B[x],
function: x:A ⟶ B[x],
universe: Type,
sub-family: F ⊆ G,
isect-family: ⋂a:A. F[a],
nat: ℕ,
apply: f a
FDL editor aliases :
type-family-continuous
Latex:
type-family-continuous\{i:l\}(P;H) == \mforall{}[X:\mBbbN{} {}\mrightarrow{} P {}\mrightarrow{} Type]. \mcap{}n:\mBbbN{}. H (X n) \msubseteq{} H \mcap{}n:\mBbbN{}. X n
Date html generated:
2016_05_14-AM-06_12_15
Last ObjectModification:
2015_09_22-PM-05_46_59
Theory : co-recursion
Home
Index