Nuprl Definition : maps-compact
maps-compact(I;J;x.f[x]) ==
∀n:{n:ℕ+| icompact(i-approx(I;n))}
∃m:{m:ℕ+| icompact(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,
real: ℝ,
nat_plus: ℕ+,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
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],
icompact: icompact(I),
nat_plus: ℕ+,
exists: ∃x:A. B[x]
FDL editor aliases :
maps-compact
Latex:
maps-compact(I;J;x.f[x]) ==
\mforall{}n:\{n:\mBbbN{}\msupplus{}| icompact(i-approx(I;n))\}
\mexists{}m:\{m:\mBbbN{}\msupplus{}| icompact(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_57_55
Last ObjectModification:
2016_08_24-PM-01_00_09
Theory : reals
Home
Index