Nuprl Definition : k-1-continuous
k-1-continuous{i:l}(k;T.F[T]) == ∀[X:ℕ ⟶ ℕk ⟶ Type]. ((∀n:ℕ. X (n + 1) ⊆ X n) ⇒ ((⋂n:ℕ. F[X n]) ⊆r F[⋂n. X n]))
Definitions occuring in Statement :
k-intersection: ⋂n. X[n],
k-subtype: A ⊆ B,
int_seg: {i..j-},
nat: ℕ,
subtype_rel: A ⊆r B,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
apply: f a,
isect: ⋂x:A. B[x],
function: x:A ⟶ B[x],
add: n + m,
natural_number: $n,
universe: Type
Definitions occuring in definition :
uall: ∀[x:A]. B[x],
function: x:A ⟶ B[x],
int_seg: {i..j-},
universe: Type,
implies: P ⇒ Q,
all: ∀x:A. B[x],
k-subtype: A ⊆ B,
add: n + m,
natural_number: $n,
subtype_rel: A ⊆r B,
isect: ⋂x:A. B[x],
nat: ℕ,
k-intersection: ⋂n. X[n],
apply: f a
FDL editor aliases :
k-1-continuous
Latex:
k-1-continuous\{i:l\}(k;T.F[T]) ==
\mforall{}[X:\mBbbN{} {}\mrightarrow{} \mBbbN{}k {}\mrightarrow{} Type]. ((\mforall{}n:\mBbbN{}. X (n + 1) \msubseteq{} X n) {}\mRightarrow{} ((\mcap{}n:\mBbbN{}. F[X n]) \msubseteq{}r F[\mcap{}n. X n]))
Date html generated:
2019_06_20-PM-01_12_48
Last ObjectModification:
2019_01_02-PM-01_36_11
Theory : co-recursion-2
Home
Index