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: P ⇒ Q,
function: x:A ⟶ B[x],
add: n + m,
natural_number: $n,
int: ℤ
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ 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 ⊆r B,
prop: ℙ,
so_apply: x[s],
ge: i ≥ j ,
nat: ℕ,
false: False,
exists: ∃x:A. B[x],
satisfiable_int_formula: satisfiable_int_formula(fmla),
not: ¬A,
uimplies: b 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 ∈ T ,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
assert: ↑b,
bnot: ¬bb,
guard: {T},
sq_type: SQType(T),
bfalse: ff,
ifthenelse: if b then t else f 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: n - 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