---

Step * 1 1 of Lemma monotone-maps-compact


1. I : Interval
2. J : Interval
3. f : I ⟶ℝ
4. (∀x,y:{t:ℝ| t ∈ I} .  ((x ≤ y) ⇒ (f[x] ≤ f[y]))) ∨ (∀x,y:{t:ℝ| t ∈ I} .  ((x ≤ y) ⇒ (f[y] ≤ f[x])))
5. ∀x:{t:ℝ| t ∈ I} . (f[x] ∈ J)
6. n : {n:ℕ+| icompact(i-approx(I;n))} 
7. icompact(i-approx(I;n))
8. i-approx(I;n) ~ [left-endpoint(i-approx(I;n)), right-endpoint(i-approx(I;n))]
9. i-approx(I;n) ⊆ I 
10. right-endpoint(i-approx(I;n)) ∈ I
11. left-endpoint(i-approx(I;n)) ∈ I
12. f[left-endpoint(i-approx(I;n))] ∈ J
13. f[right-endpoint(i-approx(I;n))] ∈ J
14. n1 : ℕ+
15. f[left-endpoint(i-approx(I;n))] ∈ i-approx(J;n1)
16. f[right-endpoint(i-approx(I;n))] ∈ i-approx(J;n1)
17. icompact(i-approx(J;n1))
18. x : ℝ
19. x ∈ i-approx(I;n)
20. left-endpoint(i-approx(I;n))≤x≤right-endpoint(i-approx(I;n))
⊢ f[x] ∈ i-approx(J;n1)
BY
{ (Assert f[left-endpoint(i-approx(I;n))]≤f[x]≤f[right-endpoint(i-approx(I;n))]
         ∨ f[right-endpoint(i-approx(I;n))]≤f[x]≤f[left-endpoint(i-approx(I;n))] BY
         (ParallelOp 4 THEN RepeatFor 2 (ParallelLast) THEN BHyp 4  THEN Auto)) }

1
1. I : Interval
2. J : Interval
3. f : I ⟶ℝ
4. (∀x,y:{t:ℝ| t ∈ I} .  ((x ≤ y) ⇒ (f[x] ≤ f[y]))) ∨ (∀x,y:{t:ℝ| t ∈ I} .  ((x ≤ y) ⇒ (f[y] ≤ f[x])))
5. ∀x:{t:ℝ| t ∈ I} . (f[x] ∈ J)
6. n : {n:ℕ+| icompact(i-approx(I;n))} 
7. icompact(i-approx(I;n))
8. i-approx(I;n) ~ [left-endpoint(i-approx(I;n)), right-endpoint(i-approx(I;n))]
9. i-approx(I;n) ⊆ I 
10. right-endpoint(i-approx(I;n)) ∈ I
11. left-endpoint(i-approx(I;n)) ∈ I
12. f[left-endpoint(i-approx(I;n))] ∈ J
13. f[right-endpoint(i-approx(I;n))] ∈ J
14. n1 : ℕ+
15. f[left-endpoint(i-approx(I;n))] ∈ i-approx(J;n1)
16. f[right-endpoint(i-approx(I;n))] ∈ i-approx(J;n1)
17. icompact(i-approx(J;n1))
18. x : ℝ
19. x ∈ i-approx(I;n)
20. left-endpoint(i-approx(I;n))≤x≤right-endpoint(i-approx(I;n))
21. f[left-endpoint(i-approx(I;n))]≤f[x]≤f[right-endpoint(i-approx(I;n))]
∨ f[right-endpoint(i-approx(I;n))]≤f[x]≤f[left-endpoint(i-approx(I;n))]
⊢ f[x] ∈ i-approx(J;n1)

---

Latex:

---

Latex:

1.  I  :  Interval
2.  J  :  Interval
3.  f  :  I  {}\mrightarrow{}\mBbbR{}
4.  (\mforall{}x,y:\{t:\mBbbR{}|  t  \mmember{}  I\}  .    ((x  \mleq{}  y)  {}\mRightarrow{}  (f[x]  \mleq{}  f[y])))
\mvee{}  (\mforall{}x,y:\{t:\mBbbR{}|  t  \mmember{}  I\}  .    ((x  \mleq{}  y)  {}\mRightarrow{}  (f[y]  \mleq{}  f[x])))
5.  \mforall{}x:\{t:\mBbbR{}|  t  \mmember{}  I\}  .  (f[x]  \mmember{}  J)
6.  n  :  \{n:\mBbbN{}\msupplus{}|  icompact(i-approx(I;n))\} 
7.  icompact(i-approx(I;n))
8.  i-approx(I;n)  \msim{}  [left-endpoint(i-approx(I;n)),  right-endpoint(i-approx(I;n))]
9.  i-approx(I;n)  \msubseteq{}  I 
10.  right-endpoint(i-approx(I;n))  \mmember{}  I
11.  left-endpoint(i-approx(I;n))  \mmember{}  I
12.  f[left-endpoint(i-approx(I;n))]  \mmember{}  J
13.  f[right-endpoint(i-approx(I;n))]  \mmember{}  J
14.  n1  :  \mBbbN{}\msupplus{}
15.  f[left-endpoint(i-approx(I;n))]  \mmember{}  i-approx(J;n1)
16.  f[right-endpoint(i-approx(I;n))]  \mmember{}  i-approx(J;n1)
17.  icompact(i-approx(J;n1))
18.  x  :  \mBbbR{}
19.  x  \mmember{}  i-approx(I;n)
20.  left-endpoint(i-approx(I;n))\mleq{}x\mleq{}right-endpoint(i-approx(I;n))
\mvdash{}  f[x]  \mmember{}  i-approx(J;n1)


By

---

Latex:
(Assert  f[left-endpoint(i-approx(I;n))]\mleq{}f[x]\mleq{}f[right-endpoint(i-approx(I;n))]
              \mvee{}  f[right-endpoint(i-approx(I;n))]\mleq{}f[x]\mleq{}f[left-endpoint(i-approx(I;n))]  BY
              (ParallelOp  4  THEN  RepeatFor  2  (ParallelLast)  THEN  BHyp  4    THEN  Auto))

---

Home Index