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: 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: 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