---

Step * of Lemma proper-continuous-implies

∀[I:Interval]. ∀[f:I ⟶ℝ].
  (f[x] (proper)continuous for x ∈ I
  ⇒ (∀m:ℕ+. (icompact(i-approx(I;m)) ⇒ iproper(i-approx(I;m)) ⇒ f[x] continuous for x ∈ i-approx(I;m))))
BY
{ (Auto THEN (D 3 With ⌜m⌝  THENA Auto) THEN (D 0 THENA Auto) THEN (RWO "i-approx-approx" 0 THENA Auto) THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[I:Interval].  \mforall{}[f:I  {}\mrightarrow{}\mBbbR{}].
    (f[x]  (proper)continuous  for  x  \mmember{}  I
    {}\mRightarrow{}  (\mforall{}m:\mBbbN{}\msupplus{}
                (icompact(i-approx(I;m))
                {}\mRightarrow{}  iproper(i-approx(I;m))
                {}\mRightarrow{}  f[x]  continuous  for  x  \mmember{}  i-approx(I;m))))


By

---

Latex:
(Auto
  THEN  (D  3  With  \mkleeneopen{}m\mkleeneclose{}    THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  (RWO  "i-approx-approx"  0  THENA  Auto)
  THEN  Trivial)

---

Home Index