### Nuprl Lemma : fun-series-converges-tail

`∀M:ℕ. ∀I:Interval. ∀f:ℕ ⟶ I ⟶ℝ.  (Σn.f[n + M;x]↓ for x ∈ I `` Σn.f[n;x]↓ for x ∈ I)`

Proof

Definitions occuring in Statement :  fun-series-converges: `Σn.f[n; x]↓ for x ∈ I` rfun: `I ⟶ℝ` interval: `Interval` nat: `ℕ` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` add: `n + m`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` fun-series-converges: `Σn.f[n; x]↓ for x ∈ I` member: `t ∈ T` so_lambda: `λ2x y.t[x; y]` rfun: `I ⟶ℝ` uall: `∀[x:A]. B[x]` nat: `ℕ` so_lambda: `λ2x.t[x]` so_apply: `x[s1;s2]` int_seg: `{i..j-}` guard: `{T}` ge: `i ≥ j ` lelt: `i ≤ j < k` and: `P ∧ Q` decidable: `Dec(P)` or: `P ∨ Q` uimplies: `b supposing a` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` top: `Top` prop: `ℙ` subtype_rel: `A ⊆r B` so_apply: `x[s]` iff: `P `⇐⇒` Q` le: `A ≤ B` less_than': `less_than'(a;b)` rev_implies: `P `` Q` fun-cauchy: `λn.f[n; x] is cauchy for x ∈ I` nat_plus: `ℕ+` int_upper: `{i...}` rneq: `x ≠ y` label: `...\$L... t` sq_stable: `SqStable(P)` squash: `↓T` subinterval: `I ⊆ J ` uiff: `uiff(P;Q)` rev_uimplies: `rev_uimplies(P;Q)`
Lemmas referenced :  fun-converges-iff-cauchy rsum_wf int_seg_properties nat_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermAdd_wf itermVar_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_add_lemma int_term_value_var_lemma int_formula_prop_wf istype-le int_seg_wf real_wf i-member_wf int_seg_subtype_nat istype-false nat_plus_properties decidable__lt intformless_wf int_formula_prop_less_lemma istype-less_than istype-int_upper i-approx_wf rleq_wf rabs_wf rsub_wf i-member-approx rdiv_wf int-to-real_wf rless-int int_upper_properties rless_wf nat_plus_wf icompact_wf fun-series-converges_wf rfun_wf interval_wf istype-nat subtract_wf sq_stable__icompact itermSubtract_wf int_term_value_subtract_lemma i-approx-is-subinterval subtype_rel_sets_simple rleq_functionality rabs_functionality rsum-difference req_weakening general_arith_equation1 rsum-shift rabs-difference-symmetry
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt sqequalHypSubstitution cut introduction extract_by_obid dependent_functionElimination thin hypothesisEquality sqequalRule lambdaEquality_alt isectElimination closedConclusion natural_numberEquality setElimination rename because_Cache hypothesis applyEquality dependent_set_memberEquality_alt addEquality productElimination unionElimination independent_isectElimination approximateComputation independent_functionElimination dependent_pairFormation_alt int_eqEquality isect_memberEquality_alt voidElimination independent_pairFormation universeIsType setIsType inhabitedIsType functionIsType inrFormation_alt imageMemberEquality baseClosed imageElimination

Latex:
\mforall{}M:\mBbbN{}.  \mforall{}I:Interval.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  I  {}\mrightarrow{}\mBbbR{}.    (\mSigma{}n.f[n  +  M;x]\mdownarrow{}  for  x  \mmember{}  I  {}\mRightarrow{}  \mSigma{}n.f[n;x]\mdownarrow{}  for  x  \mmember{}  I)

Date html generated: 2019_10_30-AM-08_59_17
Last ObjectModification: 2018_11_08-PM-02_13_18

Theory : reals

Home Index