---

Step * 2 1 1 1 1 1 1 1 of Lemma Riemann-integral-additive


1. a : ℝ
2. b : {b:ℝ| a ≤ b} 
3. f : {f:[a, b] ⟶ℝ| ifun(f;[a, b])} 
4. c : ℝ
5. a ≤ c
6. c ≤ b
7. λx.f[x] ∈ {f:[a, b] ⟶ℝ| ifun(f;[a, b])} 
8. ∫ f[x] dx on [a, c] ∈ ℝ
9. ∫ f[x] dx on [c, b] ∈ ℝ
10. m : ℕ+
11. ifun(f;[a, b])
12. ifun(f;[a, c])
13. ifun(f;[c, b])
14. N1 : ℕ
15. ∀k:ℕ
      ((N1 ≤ k)
      ⇒ (|S(λx.f[x];full-partition([a, c];uniform-partition([a, c];k + 1))) - ∫ f[x] dx on [a, c]| ≤ (r1/r(3 * m))))
16. N : ℕ
17. ∀k:ℕ
      ((N ≤ k)
      ⇒ (|S(λx.f[x];full-partition([c, b];uniform-partition([c, b];k + 1))) - ∫ f[x] dx on [c, b]| ≤ (r1/r(3 * m))))
18. d : {d:ℝ| r0 < d} 
19. ∀p:partition([a, b])
      ((partition-mesh([a, b];p) ≤ d)
      ⇒ (∀y:partition-choice(full-partition([a, b];p))
            (|S(λx.f[x];full-partition([a, b];p)) - ∫ f[x] dx on [a, b]| ≤ (r1/r(3 * m)))))
20. k : ℕ
21. p : ℝ List
22. [%17] : partitions([a, c];p)
23. q : ℝ List
24. [%18] : partitions([c, b];q)
⊢ frs-non-dec(p @ [c / q])
BY
{ ((Unhide THENA Auto) THEN (RWO "frs-non-dec-sorted-by" 0 THENA Auto) THEN RWO "sorted-by-append" 0 THEN Auto) }

1
1. a : ℝ
2. b : {b:ℝ| a ≤ b} 
3. f : {f:[a, b] ⟶ℝ| ifun(f;[a, b])} 
4. c : ℝ
5. a ≤ c
6. c ≤ b
7. λx.f[x] ∈ {f:[a, b] ⟶ℝ| ifun(f;[a, b])} 
8. ∫ f[x] dx on [a, c] ∈ ℝ
9. ∫ f[x] dx on [c, b] ∈ ℝ
10. m : ℕ+
11. ifun(f;[a, b])
12. ifun(f;[a, c])
13. ifun(f;[c, b])
14. N1 : ℕ
15. ∀k:ℕ
      ((N1 ≤ k)
      ⇒ (|S(λx.f[x];full-partition([a, c];uniform-partition([a, c];k + 1))) - ∫ f[x] dx on [a, c]| ≤ (r1/r(3 * m))))
16. N : ℕ
17. ∀k:ℕ
      ((N ≤ k)
      ⇒ (|S(λx.f[x];full-partition([c, b];uniform-partition([c, b];k + 1))) - ∫ f[x] dx on [c, b]| ≤ (r1/r(3 * m))))
18. d : {d:ℝ| r0 < d} 
19. ∀p:partition([a, b])
      ((partition-mesh([a, b];p) ≤ d)
      ⇒ (∀y:partition-choice(full-partition([a, b];p))
            (|S(λx.f[x];full-partition([a, b];p)) - ∫ f[x] dx on [a, b]| ≤ (r1/r(3 * m)))))
20. k : ℕ
21. p : ℝ List
22. partitions([a, c];p)
23. q : ℝ List
24. partitions([c, b];q)
⊢ sorted-by(λx,y. (x ≤ y);p)

2
1. a : ℝ
2. b : {b:ℝ| a ≤ b} 
3. f : {f:[a, b] ⟶ℝ| ifun(f;[a, b])} 
4. c : ℝ
5. a ≤ c
6. c ≤ b
7. λx.f[x] ∈ {f:[a, b] ⟶ℝ| ifun(f;[a, b])} 
8. ∫ f[x] dx on [a, c] ∈ ℝ
9. ∫ f[x] dx on [c, b] ∈ ℝ
10. m : ℕ+
11. ifun(f;[a, b])
12. ifun(f;[a, c])
13. ifun(f;[c, b])
14. N1 : ℕ
15. ∀k:ℕ
      ((N1 ≤ k)
      ⇒ (|S(λx.f[x];full-partition([a, c];uniform-partition([a, c];k + 1))) - ∫ f[x] dx on [a, c]| ≤ (r1/r(3 * m))))
16. N : ℕ
17. ∀k:ℕ
      ((N ≤ k)
      ⇒ (|S(λx.f[x];full-partition([c, b];uniform-partition([c, b];k + 1))) - ∫ f[x] dx on [c, b]| ≤ (r1/r(3 * m))))
18. d : {d:ℝ| r0 < d} 
19. ∀p:partition([a, b])
      ((partition-mesh([a, b];p) ≤ d)
      ⇒ (∀y:partition-choice(full-partition([a, b];p))
            (|S(λx.f[x];full-partition([a, b];p)) - ∫ f[x] dx on [a, b]| ≤ (r1/r(3 * m)))))
20. k : ℕ
21. p : ℝ List
22. partitions([a, c];p)
23. q : ℝ List
24. partitions([c, b];q)
25. sorted-by(λx,y. (x ≤ y);p)
⊢ sorted-by(λx,y. (x ≤ y);[c / q])

3
1. a : ℝ
2. b : {b:ℝ| a ≤ b} 
3. f : {f:[a, b] ⟶ℝ| ifun(f;[a, b])} 
4. c : ℝ
5. a ≤ c
6. c ≤ b
7. λx.f[x] ∈ {f:[a, b] ⟶ℝ| ifun(f;[a, b])} 
8. ∫ f[x] dx on [a, c] ∈ ℝ
9. ∫ f[x] dx on [c, b] ∈ ℝ
10. m : ℕ+
11. ifun(f;[a, b])
12. ifun(f;[a, c])
13. ifun(f;[c, b])
14. N1 : ℕ
15. ∀k:ℕ
      ((N1 ≤ k)
      ⇒ (|S(λx.f[x];full-partition([a, c];uniform-partition([a, c];k + 1))) - ∫ f[x] dx on [a, c]| ≤ (r1/r(3 * m))))
16. N : ℕ
17. ∀k:ℕ
      ((N ≤ k)
      ⇒ (|S(λx.f[x];full-partition([c, b];uniform-partition([c, b];k + 1))) - ∫ f[x] dx on [c, b]| ≤ (r1/r(3 * m))))
18. d : {d:ℝ| r0 < d} 
19. ∀p:partition([a, b])
      ((partition-mesh([a, b];p) ≤ d)
      ⇒ (∀y:partition-choice(full-partition([a, b];p))
            (|S(λx.f[x];full-partition([a, b];p)) - ∫ f[x] dx on [a, b]| ≤ (r1/r(3 * m)))))
20. k : ℕ
21. p : ℝ List
22. partitions([a, c];p)
23. q : ℝ List
24. partitions([c, b];q)
25. sorted-by(λx,y. (x ≤ y);p)
26. sorted-by(λx,y. (x ≤ y);[c / q])
⊢ (∀a∈p.(∀b∈[c / q].(λx,y. (x ≤ y)) a b))

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \{b:\mBbbR{}|  a  \mleq{}  b\} 
3.  f  :  \{f:[a,  b]  {}\mrightarrow{}\mBbbR{}|  ifun(f;[a,  b])\} 
4.  c  :  \mBbbR{}
5.  a  \mleq{}  c
6.  c  \mleq{}  b
7.  \mlambda{}x.f[x]  \mmember{}  \{f:[a,  b]  {}\mrightarrow{}\mBbbR{}|  ifun(f;[a,  b])\} 
8.  \mint{}  f[x]  dx  on  [a,  c]  \mmember{}  \mBbbR{}
9.  \mint{}  f[x]  dx  on  [c,  b]  \mmember{}  \mBbbR{}
10.  m  :  \mBbbN{}\msupplus{}
11.  ifun(f;[a,  b])
12.  ifun(f;[a,  c])
13.  ifun(f;[c,  b])
14.  N1  :  \mBbbN{}
15.  \mforall{}k:\mBbbN{}
            ((N1  \mleq{}  k)
            {}\mRightarrow{}  (|S(\mlambda{}x.f[x];full-partition([a,  c];uniform-partition([a,  c];k  +  1))) 
                  -  \mint{}  f[x]  dx  on  [a,  c]|  \mleq{}  (r1/r(3  *  m))))
16.  N  :  \mBbbN{}
17.  \mforall{}k:\mBbbN{}
            ((N  \mleq{}  k)
            {}\mRightarrow{}  (|S(\mlambda{}x.f[x];full-partition([c,  b];uniform-partition([c,  b];k  +  1))) 
                  -  \mint{}  f[x]  dx  on  [c,  b]|  \mleq{}  (r1/r(3  *  m))))
18.  d  :  \{d:\mBbbR{}|  r0  <  d\} 
19.  \mforall{}p:partition([a,  b])
            ((partition-mesh([a,  b];p)  \mleq{}  d)
            {}\mRightarrow{}  (\mforall{}y:partition-choice(full-partition([a,  b];p))
                        (|S(\mlambda{}x.f[x];full-partition([a,  b];p))  -  \mint{}  f[x]  dx  on  [a,  b]|  \mleq{}  (r1/r(3  *  m)))))
20.  k  :  \mBbbN{}
21.  p  :  \mBbbR{}  List
22.  [\%17]  :  partitions([a,  c];p)
23.  q  :  \mBbbR{}  List
24.  [\%18]  :  partitions([c,  b];q)
\mvdash{}  frs-non-dec(p  @  [c  /  q])


By

---

Latex:
((Unhide  THENA  Auto)
  THEN  (RWO  "frs-non-dec-sorted-by"  0  THENA  Auto)
  THEN  RWO  "sorted-by-append"  0
  THEN  Auto)

---

Home Index