---

Step * of Lemma proper-continuous-is-continuous

∀I:Interval. (iproper(I) ⇒ (∀f:I ⟶ℝ. (f[x] (proper)continuous for x ∈ I ⇒ f[x] continuous for x ∈ I)))
BY
{ (((Auto THEN D 0) THENA Auto) THEN (D -2 With ⌜m + 1⌝  THENA ((D -1 THEN MemTypeCD) THEN EAuto 1))) }

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))))))})
⊢ ∀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:
\mforall{}I:Interval
    (iproper(I)  {}\mRightarrow{}  (\mforall{}f:I  {}\mrightarrow{}\mBbbR{}.  (f[x]  (proper)continuous  for  x  \mmember{}  I  {}\mRightarrow{}  f[x]  continuous  for  x  \mmember{}  I)))


By

---

Latex:
(((Auto  THEN  D  0)  THENA  Auto)  THEN  (D  -2  With  \mkleeneopen{}m  +  1\mkleeneclose{}    THENA  ((D  -1  THEN  MemTypeCD)  THEN  EAuto  1)))

---

Home Index