### Nuprl Lemma : fun-converges-on-compact

`∀I:Interval. ∀f:ℕ ⟶ I ⟶ℝ.`
`  ((∀m:{m:ℕ+| icompact(i-approx(I;m))} . λn.f[n;x]↓ for x ∈ i-approx(I;m))) `` λn.f[n;x]↓ for x ∈ I))`

Proof

Definitions occuring in Statement :  fun-converges: `λn.f[n; x]↓ for x ∈ I)` icompact: `icompact(I)` rfun: `I ⟶ℝ` i-approx: `i-approx(I;n)` interval: `Interval` nat_plus: `ℕ+` nat: `ℕ` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` implies: `P `` Q` set: `{x:A| B[x]} ` function: `x:A ⟶ B[x]`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` so_lambda: `λ2x y.t[x; y]` rfun: `I ⟶ℝ` so_apply: `x[s1;s2]` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` prop: `ℙ` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` fun-cauchy: `λn.f[n; x] is cauchy for x ∈ I` so_lambda: `λ2x.t[x]` so_apply: `x[s]` uimplies: `b supposing a` subinterval: `I ⊆ J ` label: `...\$L... t` nat_plus: `ℕ+` less_than: `a < b` squash: `↓T` less_than': `less_than'(a;b)` true: `True` top: `Top`
Lemmas referenced :  i-approx-approx less_than_wf i-member-approx fun-converges_wf all_wf icompact_wf nat_plus_wf subtype_rel_sets i-approx_wf i-approx-is-subinterval nat_wf i-member_wf real_wf rfun_wf fun-converges-iff-cauchy
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality sqequalRule lambdaEquality applyEquality hypothesis isectElimination setEquality productElimination independent_functionElimination setElimination rename because_Cache independent_isectElimination dependent_set_memberEquality functionEquality natural_numberEquality independent_pairFormation introduction imageMemberEquality baseClosed isect_memberEquality voidElimination voidEquality

Latex:
\mforall{}I:Interval.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  I  {}\mrightarrow{}\mBbbR{}.
((\mforall{}m:\{m:\mBbbN{}\msupplus{}|  icompact(i-approx(I;m))\}  .  \mlambda{}n.f[n;x]\mdownarrow{}  for  x  \mmember{}  i-approx(I;m)))  {}\mRightarrow{}  \mlambda{}n.f[n;x]\mdownarrow{}  for  x  \mmember{}  I)\000C)

Date html generated: 2016_05_18-AM-09_54_15
Last ObjectModification: 2016_01_17-AM-02_53_59

Theory : reals

Home Index