Nuprl Definition : maps-compact-proper

maps-compact-proper(I;J;x.f[x]) ==
  ∀n:{n:ℕ+icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n))} 
    ∃m:{m:ℕ+icompact(i-approx(J;m)) ∧ iproper(i-approx(J;m))} . ∀x:{x:ℝx ∈ i-approx(I;n)} (f[x] ∈ i-approx(J;m))



Definitions occuring in Statement :  icompact: icompact(I) i-approx: i-approx(I;n) i-member: r ∈ I iproper: iproper(I) real: nat_plus: + all: x:A. B[x] exists: x:A. B[x] and: P ∧ Q set: {x:A| B[x]} 
Definitions occuring in definition :  i-approx: i-approx(I;n) i-member: r ∈ I real: set: {x:A| B[x]}  all: x:A. B[x] iproper: iproper(I) icompact: icompact(I) and: P ∧ Q nat_plus: + exists: x:A. B[x]
FDL editor aliases :  maps-compact-proper

Latex:
maps-compact-proper(I;J;x.f[x])  ==
    \mforall{}n:\{n:\mBbbN{}\msupplus{}|  icompact(i-approx(I;n))  \mwedge{}  iproper(i-approx(I;n))\} 
        \mexists{}m:\{m:\mBbbN{}\msupplus{}|  icompact(i-approx(J;m))  \mwedge{}  iproper(i-approx(J;m))\} 
          \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  i-approx(I;n)\}  .  (f[x]  \mmember{}  i-approx(J;m))



Date html generated: 2016_10_26-AM-09_58_17
Last ObjectModification: 2016_08_24-PM-00_55_52

Theory : reals


Home Index