---

Step * 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))
⊢ ∃m:{m:ℕ+| icompact(i-approx(J;m))} . ∀x:{x:ℝ| x ∈ i-approx(I;n)} . (f[x] ∈ i-approx(J;m))
BY
{ (D 0 With ⌜n1⌝ 
   THEN Auto
   THEN D -1
   THEN (Unhide THENA Auto)
   THEN DupHyp (-1)
   THEN (RWO "i-member-compact" (-1) THENA 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))
⊢ 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))
\mvdash{}  \mexists{}m:\{m:\mBbbN{}\msupplus{}|  icompact(i-approx(J;m))\}  .  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  i-approx(I;n)\}  .  (f[x]  \mmember{}  i-approx(J;m))


By

---

Latex:
(D  0  With  \mkleeneopen{}n1\mkleeneclose{} 
  THEN  Auto
  THEN  D  -1
  THEN  (Unhide  THENA  Auto)
  THEN  DupHyp  (-1)
  THEN  (RWO  "i-member-compact"  (-1)  THENA  Auto))

---

Home Index