---

Step * 1 of Lemma continuous-composition-from-maps-compact


1. I : Interval
2. J : Interval
3. f : I ⟶ℝ
4. g : J ⟶ℝ
5. m : {m:ℕ+| icompact(i-approx(I;m))} 
6. n : ℕ+
7. ∀n:ℕ+
     (∃d:ℝ [((r0 < d)
           ∧ (∀x,y:ℝ.  ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(n))))))])
8. M : {m:ℕ+| icompact(i-approx(J;m))} 
9. ∀x:{x:ℝ| x ∈ i-approx(I;m)} . (f[x] ∈ i-approx(J;M))
10. ∀n:ℕ+
      (∃d:ℝ [((r0 < d)
            ∧ (∀x,y:ℝ.  ((x ∈ i-approx(J;M)) ⇒ (y ∈ i-approx(J;M)) ⇒ (|x - y| ≤ d) ⇒ (|g[x] - g[y]| ≤ (r1/r(n))))))])
11. d : ℝ
12. [%9] : (r0 < d)
∧ (∀x,y:ℝ.  ((x ∈ i-approx(J;M)) ⇒ (y ∈ i-approx(J;M)) ⇒ (|x - y| ≤ d) ⇒ (|g[x] - g[y]| ≤ (r1/r(n)))))
13. k : ℕ+
14. (r1/r(k)) < d
⊢ ∃d:ℝ [((r0 < d)
       ∧ (∀x,y:ℝ.  ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d) ⇒ (|g[f[x]] - g[f[y]]| ≤ (r1/r(n))))))]
BY
{ ((InstHyp [⌜k⌝] 7⋅ THENA Auto) THEN ParallelLast) }

1
.....set predicate..... 
1. I : Interval
2. J : Interval
3. f : I ⟶ℝ
4. g : J ⟶ℝ
5. m : {m:ℕ+| icompact(i-approx(I;m))} 
6. n : ℕ+
7. ∀n:ℕ+
     (∃d:ℝ [((r0 < d)
           ∧ (∀x,y:ℝ.  ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(n))))))])
8. M : {m:ℕ+| icompact(i-approx(J;m))} 
9. ∀x:{x:ℝ| x ∈ i-approx(I;m)} . (f[x] ∈ i-approx(J;M))
10. ∀n:ℕ+
      (∃d:ℝ [((r0 < d)
            ∧ (∀x,y:ℝ.  ((x ∈ i-approx(J;M)) ⇒ (y ∈ i-approx(J;M)) ⇒ (|x - y| ≤ d) ⇒ (|g[x] - g[y]| ≤ (r1/r(n))))))])
11. d : ℝ
12. (r0 < d) ∧ (∀x,y:ℝ.  ((x ∈ i-approx(J;M)) ⇒ (y ∈ i-approx(J;M)) ⇒ (|x - y| ≤ d) ⇒ (|g[x] - g[y]| ≤ (r1/r(n)))))
13. k : ℕ+
14. (r1/r(k)) < d
15. d1 : ℝ
16. (r0 < d1) ∧ (∀x,y:ℝ.  ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d1) ⇒ (|f[x] - f[y]| ≤ (r1/r(k)))))
⊢ (r0 < d1)
∧ (∀x,y:ℝ.  ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d1) ⇒ (|g[f[x]] - g[f[y]]| ≤ (r1/r(n)))))

2
1. I : Interval
2. J : Interval
3. f : I ⟶ℝ
4. g : J ⟶ℝ
5. m : {m:ℕ+| icompact(i-approx(I;m))} 
6. n : ℕ+
7. ∀n:ℕ+
     (∃d:ℝ [((r0 < d)
           ∧ (∀x,y:ℝ.  ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(n))))))])
8. M : {m:ℕ+| icompact(i-approx(J;m))} 
9. ∀x:{x:ℝ| x ∈ i-approx(I;m)} . (f[x] ∈ i-approx(J;M))
10. ∀n:ℕ+
      (∃d:ℝ [((r0 < d)
            ∧ (∀x,y:ℝ.  ((x ∈ i-approx(J;M)) ⇒ (y ∈ i-approx(J;M)) ⇒ (|x - y| ≤ d) ⇒ (|g[x] - g[y]| ≤ (r1/r(n))))))])
11. d : ℝ
12. r0 < d
13. ∀x,y:ℝ.  ((x ∈ i-approx(J;M)) ⇒ (y ∈ i-approx(J;M)) ⇒ (|x - y| ≤ d) ⇒ (|g[x] - g[y]| ≤ (r1/r(n))))
14. k : ℕ+
15. (r1/r(k)) < d
16. d1 : ℝ
17. r0 < d1
18. ∀x,y:ℝ.  ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d1) ⇒ (|f[x] - f[y]| ≤ (r1/r(k))))
19. d2 : ℝ
20. x : r0 < d2
21. x1 : ℝ
22. y : ℝ
23. x2 : x1 ∈ i-approx(I;m)
24. x3 : y ∈ i-approx(I;m)
25. x4 : |x1 - y| ≤ d2
⊢ f[x1] ∈ {x:ℝ| x ∈ J} 

3
1. I : Interval
2. J : Interval
3. f : I ⟶ℝ
4. g : J ⟶ℝ
5. m : {m:ℕ+| icompact(i-approx(I;m))} 
6. n : ℕ+
7. ∀n:ℕ+
     (∃d:ℝ [((r0 < d)
           ∧ (∀x,y:ℝ.  ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(n))))))])
8. M : {m:ℕ+| icompact(i-approx(J;m))} 
9. ∀x:{x:ℝ| x ∈ i-approx(I;m)} . (f[x] ∈ i-approx(J;M))
10. ∀n:ℕ+
      (∃d:ℝ [((r0 < d)
            ∧ (∀x,y:ℝ.  ((x ∈ i-approx(J;M)) ⇒ (y ∈ i-approx(J;M)) ⇒ (|x - y| ≤ d) ⇒ (|g[x] - g[y]| ≤ (r1/r(n))))))])
11. d : ℝ
12. r0 < d
13. ∀x,y:ℝ.  ((x ∈ i-approx(J;M)) ⇒ (y ∈ i-approx(J;M)) ⇒ (|x - y| ≤ d) ⇒ (|g[x] - g[y]| ≤ (r1/r(n))))
14. k : ℕ+
15. (r1/r(k)) < d
16. d1 : ℝ
17. r0 < d1
18. ∀x,y:ℝ.  ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d1) ⇒ (|f[x] - f[y]| ≤ (r1/r(k))))
19. d2 : ℝ
20. x : r0 < d2
21. x1 : ℝ
22. y : ℝ
23. x2 : x1 ∈ i-approx(I;m)
24. x3 : y ∈ i-approx(I;m)
25. x4 : |x1 - y| ≤ d2
⊢ f[y] ∈ {x:ℝ| x ∈ J} 

---

Latex:

---

Latex:

1.  I  :  Interval
2.  J  :  Interval
3.  f  :  I  {}\mrightarrow{}\mBbbR{}
4.  g  :  J  {}\mrightarrow{}\mBbbR{}
5.  m  :  \{m:\mBbbN{}\msupplus{}|  icompact(i-approx(I;m))\} 
6.  n  :  \mBbbN{}\msupplus{}
7.  \mforall{}n:\mBbbN{}\msupplus{}
          (\mexists{}d:\mBbbR{}  [((r0  <  d)
                      \mwedge{}  (\mforall{}x,y:\mBbbR{}.
                                ((x  \mmember{}  i-approx(I;m))
                                {}\mRightarrow{}  (y  \mmember{}  i-approx(I;m))
                                {}\mRightarrow{}  (|x  -  y|  \mleq{}  d)
                                {}\mRightarrow{}  (|f[x]  -  f[y]|  \mleq{}  (r1/r(n))))))])
8.  M  :  \{m:\mBbbN{}\msupplus{}|  icompact(i-approx(J;m))\} 
9.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  i-approx(I;m)\}  .  (f[x]  \mmember{}  i-approx(J;M))
10.  \mforall{}n:\mBbbN{}\msupplus{}
            (\mexists{}d:\mBbbR{}  [((r0  <  d)
                        \mwedge{}  (\mforall{}x,y:\mBbbR{}.
                                  ((x  \mmember{}  i-approx(J;M))
                                  {}\mRightarrow{}  (y  \mmember{}  i-approx(J;M))
                                  {}\mRightarrow{}  (|x  -  y|  \mleq{}  d)
                                  {}\mRightarrow{}  (|g[x]  -  g[y]|  \mleq{}  (r1/r(n))))))])
11.  d  :  \mBbbR{}
12.  [\%9]  :  (r0  <  d)
\mwedge{}  (\mforall{}x,y:\mBbbR{}.
          ((x  \mmember{}  i-approx(J;M))  {}\mRightarrow{}  (y  \mmember{}  i-approx(J;M))  {}\mRightarrow{}  (|x  -  y|  \mleq{}  d)  {}\mRightarrow{}  (|g[x]  -  g[y]|  \mleq{}  (r1/r(n)))))
13.  k  :  \mBbbN{}\msupplus{}
14.  (r1/r(k))  <  d
\mvdash{}  \mexists{}d:\mBbbR{}  [((r0  <  d)
              \mwedge{}  (\mforall{}x,y:\mBbbR{}.
                        ((x  \mmember{}  i-approx(I;m))
                        {}\mRightarrow{}  (y  \mmember{}  i-approx(I;m))
                        {}\mRightarrow{}  (|x  -  y|  \mleq{}  d)
                        {}\mRightarrow{}  (|g[f[x]]  -  g[f[y]]|  \mleq{}  (r1/r(n))))))]


By

---

Latex:
((InstHyp  [\mkleeneopen{}k\mkleeneclose{}]  7\mcdot{}  THENA  Auto)  THEN  ParallelLast)

---

Home Index