Nuprl Definition : rel-continuous
rel-continuous{i:l}(T;R.F[R]) == ∀R:ℕ ⟶ T ⟶ T ⟶ ℙ. isect-rel(ℕ;n.F[R n]) => F[isect-rel(ℕ;n.R n)]
Definitions occuring in Statement :
isect-rel: isect-rel(T;i.R[i]),
rel_implies: R1 => R2,
nat: ℕ,
prop: ℙ,
all: ∀x:A. B[x],
apply: f a,
function: x:A ⟶ B[x]
Definitions occuring in definition :
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
prop: ℙ,
rel_implies: R1 => R2,
isect-rel: isect-rel(T;i.R[i]),
nat: ℕ,
apply: f a
FDL editor aliases :
rel-continuous
Latex:
rel-continuous\{i:l\}(T;R.F[R]) ==
\mforall{}R:\mBbbN{} {}\mrightarrow{} T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}. isect-rel(\mBbbN{};n.F[R n]) => F[isect-rel(\mBbbN{};n.R n)]
Date html generated:
2016_05_14-AM-06_04_57
Last ObjectModification:
2015_09_22-PM-05_46_50
Theory : relations
Home
Index