---

Step * 1 of Lemma proper-continuous-is-continuous


1. I : Interval
2. iproper(I)
3. f : I ⟶ℝ
4. m : {m:ℕ+| icompact(i-approx(I;m))} 
5. ∀n:ℕ+
     (∃d:{ℝ| ((r0 < d)
             ∧ (∀x,y:ℝ.
                  ((x ∈ i-approx(I;m + 1))
                  ⇒ (y ∈ i-approx(I;m + 1))
                  ⇒ (|x - y| ≤ d)
                  ⇒ (|f[x] - f[y]| ≤ (r1/r(n))))))})
⊢ ∀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))))))})
BY
{ (Assert i-approx(I;m) ⊆ i-approx(I;m + 1)  BY
         ((InstLemma `i-approx-monotonic` [⌜I⌝;⌜m⌝;⌜m + 1⌝]⋅ THENA Auto) THEN D 0 THEN Auto)) }

1
1. I : Interval
2. iproper(I)
3. f : I ⟶ℝ
4. m : {m:ℕ+| icompact(i-approx(I;m))} 
5. ∀n:ℕ+
     (∃d:{ℝ| ((r0 < d)
             ∧ (∀x,y:ℝ.
                  ((x ∈ i-approx(I;m + 1))
                  ⇒ (y ∈ i-approx(I;m + 1))
                  ⇒ (|x - y| ≤ d)
                  ⇒ (|f[x] - f[y]| ≤ (r1/r(n))))))})
6. i-approx(I;m) ⊆ i-approx(I;m + 1) 
⊢ ∀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))))))})

---

Latex:

---

Latex:

1.  I  :  Interval
2.  iproper(I)
3.  f  :  I  {}\mrightarrow{}\mBbbR{}
4.  m  :  \{m:\mBbbN{}\msupplus{}|  icompact(i-approx(I;m))\} 
5.  \mforall{}n:\mBbbN{}\msupplus{}
          (\mexists{}d:\{\mBbbR{}|  ((r0  <  d)
                          \mwedge{}  (\mforall{}x,y:\mBbbR{}.
                                    ((x  \mmember{}  i-approx(I;m  +  1))
                                    {}\mRightarrow{}  (y  \mmember{}  i-approx(I;m  +  1))
                                    {}\mRightarrow{}  (|x  -  y|  \mleq{}  d)
                                    {}\mRightarrow{}  (|f[x]  -  f[y]|  \mleq{}  (r1/r(n))))))\})
\mvdash{}  \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))))))\})


By

---

Latex:
(Assert  i-approx(I;m)  \msubseteq{}  i-approx(I;m  +  1)    BY
              ((InstLemma  `i-approx-monotonic`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}m  +  1\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  D  0  THEN  Auto))

---

Home Index