---

Step * of Lemma monotone-maps-compact

∀I,J:Interval. ∀f:I ⟶ℝ.
  (((∀x,y:{t:ℝ| t ∈ I} .  ((x ≤ y) ⇒ (f[x] ≤ f[y]))) ∨ (∀x,y:{t:ℝ| t ∈ I} .  ((x ≤ y) ⇒ (f[y] ≤ f[x]))))
  ⇒ (∀x:{t:ℝ| t ∈ I} . (f[x] ∈ J))
  ⇒ maps-compact(I;J;x.f[x]))
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN (Assert icompact(i-approx(I;n)) BY
               Auto)
   THEN (InstLemma `icompact-is-rccint` [⌜i-approx(I;n)⌝]⋅ THENA Auto)
   THEN ((Assert i-approx(I;n) ⊆ I  BY
                Auto)
         THEN (Assert right-endpoint(i-approx(I;n)) ∈ I BY
                     (BackThruSomeHyp' THEN EAuto 1))
         THEN (Assert left-endpoint(i-approx(I;n)) ∈ I BY
                     (BackThruSomeHyp' THEN EAuto 1)))
   THEN (Assert (f[left-endpoint(i-approx(I;n))] ∈ J) ∧ (f[right-endpoint(i-approx(I;n))] ∈ J) BY
               (D 0 THEN BackThruSomeHyp THEN Auto))
   THEN (FLemma `i-approx-containing2` [-1] THENA (Auto THEN (MemTypeCD THEN Auto) THEN BackThruSomeHyp' THEN EAuto 1))
   THEN ExRepD
   THEN (Assert icompact(i-approx(J;n1)) BY
               ((D 0 THEN Auto) THEN D 0 With ⌜f[left-endpoint(i-approx(I;n))]⌝  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))
⊢ ∃m:{m:ℕ+| icompact(i-approx(J;m))} . ∀x:{x:ℝ| x ∈ i-approx(I;n)} . (f[x] ∈ i-approx(J;m))

---

Latex:

---

Latex:
\mforall{}I,J:Interval.  \mforall{}f:I  {}\mrightarrow{}\mBbbR{}.
    (((\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]))))
    {}\mRightarrow{}  (\mforall{}x:\{t:\mBbbR{}|  t  \mmember{}  I\}  .  (f[x]  \mmember{}  J))
    {}\mRightarrow{}  maps-compact(I;J;x.f[x]))


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  (Assert  icompact(i-approx(I;n))  BY
                          Auto)
  THEN  (InstLemma  `icompact-is-rccint`  [\mkleeneopen{}i-approx(I;n)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ((Assert  i-approx(I;n)  \msubseteq{}  I    BY
                            Auto)
              THEN  (Assert  right-endpoint(i-approx(I;n))  \mmember{}  I  BY
                                      (BackThruSomeHyp'  THEN  EAuto  1))
              THEN  (Assert  left-endpoint(i-approx(I;n))  \mmember{}  I  BY
                                      (BackThruSomeHyp'  THEN  EAuto  1)))
  THEN  (Assert  (f[left-endpoint(i-approx(I;n))]  \mmember{}  J)  \mwedge{}  (f[right-endpoint(i-approx(I;n))]  \mmember{}  J)  BY
                          (D  0  THEN  BackThruSomeHyp  THEN  Auto))
  THEN  (FLemma  `i-approx-containing2`  [-1]
              THENA  (Auto  THEN  (MemTypeCD  THEN  Auto)  THEN  BackThruSomeHyp'  THEN  EAuto  1)
              )
  THEN  ExRepD
  THEN  (Assert  icompact(i-approx(J;n1))  BY
                          ((D  0  THEN  Auto)  THEN  D  0  With  \mkleeneopen{}f[left-endpoint(i-approx(I;n))]\mkleeneclose{}    THEN  Auto)))

---

Home Index