---

Step * 1 1 of Lemma integral_wf


1. a : ℝ@i
2. b : ℝ@i
3. a ≤ b@i
4. f : [a, b] ⟶ℝ@i
5. mc : f x continuous for x ∈ [a, b]@i
6. v : ∀f:[a, b] ⟶ℝ. ∀mc:f[x] continuous for x ∈ [a, b].  Riemann-sum-alt(f;a;b;k + 1)↓ as k→∞@i
7. (TERMOF{alt-Riemann-sums-converge-ext:o, 1:l} a b)
= v
∈ (∀f:[a, b] ⟶ℝ. ∀mc:f[x] continuous for x ∈ [a, b].  Riemann-sum-alt(f;a;b;k + 1)↓ as k→∞)@i
⊢ v (λx.(f x)) ∈ mc:λx.(f x)[x] continuous for x ∈ [a, b] ⟶ Riemann-sum-alt(λx.(f x);a;b;k + 1)↓ as k→∞
BY
{ Fold `all` 0 }

1
1. a : ℝ@i
2. b : ℝ@i
3. a ≤ b@i
4. f : [a, b] ⟶ℝ@i
5. mc : f x continuous for x ∈ [a, b]@i
6. v : ∀f:[a, b] ⟶ℝ. ∀mc:f[x] continuous for x ∈ [a, b].  Riemann-sum-alt(f;a;b;k + 1)↓ as k→∞@i
7. (TERMOF{alt-Riemann-sums-converge-ext:o, 1:l} a b)
= v
∈ (∀f:[a, b] ⟶ℝ. ∀mc:f[x] continuous for x ∈ [a, b].  Riemann-sum-alt(f;a;b;k + 1)↓ as k→∞)@i
⊢ v (λx.(f x)) ∈ ∀mc:λx.(f x)[x] continuous for x ∈ [a, b]. Riemann-sum-alt(λx.(f x);a;b;k + 1)↓ as k→∞

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}@i
2.  b  :  \mBbbR{}@i
3.  a  \mleq{}  b@i
4.  f  :  [a,  b]  {}\mrightarrow{}\mBbbR{}@i
5.  mc  :  f  x  continuous  for  x  \mmember{}  [a,  b]@i
6.  v  :  \mforall{}f:[a,  b]  {}\mrightarrow{}\mBbbR{}.  \mforall{}mc:f[x]  continuous  for  x  \mmember{}  [a,  b].    Riemann-sum-alt(f;a;b;k  +  1)\mdownarrow{}  as  k\mrightarrow{}\minfty{}@i
7.  (TERMOF\{alt-Riemann-sums-converge-ext:o,  1:l\}  a  b)  =  v@i
\mvdash{}  v  (\mlambda{}x.(f  x))  \mmember{}  mc:\mlambda{}x.(f  x)[x]  continuous  for  x  \mmember{}  [a,  b]
    {}\mrightarrow{}  Riemann-sum-alt(\mlambda{}x.(f  x);a;b;k  +  1)\mdownarrow{}  as  k\mrightarrow{}\minfty{}


By

---

Latex:
Fold  `all`  0

---

Home Index