---

Step * of Lemma integral_wf

∀[a,b:ℝ]. ∀[f:{f:[rmin(a;b), rmax(a;b)] ⟶ℝ| ifun(f;[rmin(a;b), rmax(a;b)])} ].  (a_∫-b f[x] dx ∈ ℝ)
BY
{ (Auto
   THEN (Assert λx.f[x] ∈ {f:[rmin(a;b), rmax(a;b)] ⟶ℝ| ifun(f;[rmin(a;b), rmax(a;b)])}  BY
               (DVar `f'⋅ THEN MemTypeCD THEN Auto))
   ) }

1
1. a : ℝ
2. b : ℝ
3. f : {f:[rmin(a;b), rmax(a;b)] ⟶ℝ| ifun(f;[rmin(a;b), rmax(a;b)])} 
4. λx.f[x] ∈ {f:[rmin(a;b), rmax(a;b)] ⟶ℝ| ifun(f;[rmin(a;b), rmax(a;b)])} 
⊢ a_∫-b f[x] dx ∈ ℝ

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbR{}].  \mforall{}[f:\{f:[rmin(a;b),  rmax(a;b)]  {}\mrightarrow{}\mBbbR{}|  ifun(f;[rmin(a;b),  rmax(a;b)])\}  ].    (a\_\mint{}\msupminus{}b  f[x]  dx  \mmember{}  \mBbbR{})


By

---

Latex:
(Auto
  THEN  (Assert  \mlambda{}x.f[x]  \mmember{}  \{f:[rmin(a;b),  rmax(a;b)]  {}\mrightarrow{}\mBbbR{}|  ifun(f;[rmin(a;b),  rmax(a;b)])\}    BY
                          (DVar  `f'\mcdot{}  THEN  MemTypeCD  THEN  Auto))
  )

---

Home Index