Nuprl Lemma : continuous-sum

I:Interval. ∀n,m:ℤ. ∀f:{n..m 1-} ⟶ I ⟶ℝ.
  ((∀i:{n..m 1-}. f[i;x] continuous for x ∈ I)  Σ{f[i;x] n≤i≤m} continuous for x ∈ I)


Proof




Definitions occuring in Statement :  continuous: f[x] continuous for x ∈ I rfun: I ⟶ℝ interval: Interval rsum: Σ{x[k] n≤k≤m} int_seg: {i..j-} so_apply: x[s1;s2] all: x:A. B[x] implies:  Q function: x:A ⟶ B[x] add: m natural_number: $n int:
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q member: t ∈ T uall: [x:A]. B[x] so_lambda: λ2x.t[x] label: ...$L... t rfun: I ⟶ℝ so_apply: x[s1;s2] subtype_rel: A ⊆B prop: so_apply: x[s] ge: i ≥  nat: false: False exists: x:A. B[x] satisfiable_int_formula: satisfiable_int_formula(fmla) not: ¬A uimplies: supposing a or: P ∨ Q decidable: Dec(P) squash: T less_than: a < b and: P ∧ Q lelt: i ≤ j < k int_seg: {i..j-} nequal: a ≠ b ∈  iff: ⇐⇒ Q rev_implies:  Q assert: b bnot: ¬bb guard: {T} sq_type: SQType(T) bfalse: ff ifthenelse: if then else fi  uiff: uiff(P;Q) btrue: tt it: unit: Unit bool: 𝔹 r-ap: f(x) rfun-eq: rfun-eq(I;f;g) rev_uimplies: rev_uimplies(P;Q) true: True subtract: m stable: Stable{P}

Latex:
\mforall{}I:Interval.  \mforall{}n,m:\mBbbZ{}.  \mforall{}f:\{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  I  {}\mrightarrow{}\mBbbR{}.
    ((\mforall{}i:\{n..m  +  1\msupminus{}\}.  f[i;x]  continuous  for  x  \mmember{}  I)  {}\mRightarrow{}  \mSigma{}\{f[i;x]  |  n\mleq{}i\mleq{}m\}  continuous  for  x  \mmember{}  I)



Date html generated: 2020_05_20-PM-00_14_27
Last ObjectModification: 2020_01_02-PM-01_58_28

Theory : reals


Home Index