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