---

Step * 1 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
{ (Unfold `member` 0
   THEN Refine `applyEquality` [mk_term_arg ⌜g:[a, b] ⟶ℝ ⟶ (∀mc:g[x] continuous for x ∈ [a, b]
                                                                Riemann-sum-alt(g;a;b;k + 1)↓ as k→∞)⌝]⋅
   THEN Auto) }

---

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{}  \mforall{}mc:\mlambda{}x.(f  x)[x]  continuous  for  x  \mmember{}  [a,  b]
                                      Riemann-sum-alt(\mlambda{}x.(f  x);a;b;k  +  1)\mdownarrow{}  as  k\mrightarrow{}\minfty{}


By

---

Latex:
(Unfold  `member`  0
  THEN  Refine  `applyEquality`  [mk\_term\_arg  \mkleeneopen{}g:[a,  b]  {}\mrightarrow{}\mBbbR{}  {}\mrightarrow{}  (\mforall{}mc:g[x]  continuous  for  x  \mmember{}  [a,  b]
                                                                                                                            Riemann-sum-alt(g;a;b;k  +  1)\mdownarrow{}  as  k\mrightarrow{}\minfty{})\mkleeneclose{}
  ]\mcdot{}
  THEN  Auto)

---

Home Index