---

Step * of Lemma integral_wf

∀a:ℝ. ∀b:{b:ℝ| a ≤ b} . ∀f:[a, b] ⟶ℝ. ∀mc:f[x] continuous for x ∈ [a, b].  (∫ f[x] dx on [a, b] ∈ ℝ)
BY
{ (RepUR ``so_apply`` 0 THEN ProveWfLemma) }

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
⊢ TERMOF{alt-Riemann-sums-converge-ext:o, 1:l} a b (λ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:
\mforall{}a:\mBbbR{}.  \mforall{}b:\{b:\mBbbR{}|  a  \mleq{}  b\}  .  \mforall{}f:[a,  b]  {}\mrightarrow{}\mBbbR{}.  \mforall{}mc:f[x]  continuous  for  x  \mmember{}  [a,  b].    (\mint{}  f[x]  dx  on  [a,  b]  \mmember{}  \mBbbR{}\000C)


By

---

Latex:
(RepUR  ``so\_apply``  0  THEN  ProveWfLemma)

---

Home Index