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