---

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

∀I,J:Interval. ∀f:I ⟶ℝ. ∀g:J ⟶ℝ.
  (maps-compact(I;J;x.f[x]) ⇒ f[x] continuous for x ∈ I ⇒ g[x] continuous for x ∈ J ⇒ g[f[x]] continuous for x ∈ I)
BY
{ TACTIC:(Auto
          THEN (D 0 THEN Auto)
          THEN (With ⌜m⌝ (D 6)⋅ THENA Auto)
          THEN (With ⌜m⌝ (D 5)⋅ THENA Auto)
          THEN D -1
          THEN RenameVar `M' (-2)
          THEN (With ⌜M⌝ (D 5)⋅ THENA Auto)
          THEN (InstHyp [⌜n⌝] (-1)⋅ THENA Auto)
          THEN D -1
          THEN InstLemma `small-reciprocal-real` [⌜d⌝]⋅
          THEN Auto
          THEN D -1) }

1
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))))))]

---

Latex:

---

Latex:
\mforall{}I,J:Interval.  \mforall{}f:I  {}\mrightarrow{}\mBbbR{}.  \mforall{}g:J  {}\mrightarrow{}\mBbbR{}.
    (maps-compact(I;J;x.f[x])
    {}\mRightarrow{}  f[x]  continuous  for  x  \mmember{}  I
    {}\mRightarrow{}  g[x]  continuous  for  x  \mmember{}  J
    {}\mRightarrow{}  g[f[x]]  continuous  for  x  \mmember{}  I)


By

---

Latex:
TACTIC:(Auto
                THEN  (D  0  THEN  Auto)
                THEN  (With  \mkleeneopen{}m\mkleeneclose{}  (D  6)\mcdot{}  THENA  Auto)
                THEN  (With  \mkleeneopen{}m\mkleeneclose{}  (D  5)\mcdot{}  THENA  Auto)
                THEN  D  -1
                THEN  RenameVar  `M'  (-2)
                THEN  (With  \mkleeneopen{}M\mkleeneclose{}  (D  5)\mcdot{}  THENA  Auto)
                THEN  (InstHyp  [\mkleeneopen{}n\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
                THEN  D  -1
                THEN  InstLemma  `small-reciprocal-real`  [\mkleeneopen{}d\mkleeneclose{}]\mcdot{}
                THEN  Auto
                THEN  D  -1)

---

Home Index