---

Step * of Lemma continuous-rinv

∀I:Interval. ∀f:I ⟶ℝ.  (f[x] continuous for x ∈ I ⇒ f[x]≠r0 for x ∈ I ⇒ (r1/f[x]) continuous for x ∈ I)
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN (With ⌜m⌝ (D 4)⋅ THENA Auto)
   THEN (With ⌜m⌝ (D 3)⋅ THENA Auto)
   THEN D 5
   THEN (UnhideSqStableHyp 6
         THENA (Auto THEN OnMaybeHyp 11 (\h. (FLemma `i-member-approx` [h] THEN Complete (Auto))))
         )) }

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

---

Latex:

---

Latex:
\mforall{}I:Interval.  \mforall{}f:I  {}\mrightarrow{}\mBbbR{}.
    (f[x]  continuous  for  x  \mmember{}  I  {}\mRightarrow{}  f[x]\mneq{}r0  for  x  \mmember{}  I  {}\mRightarrow{}  (r1/f[x])  continuous  for  x  \mmember{}  I)


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  (With  \mkleeneopen{}m\mkleeneclose{}  (D  4)\mcdot{}  THENA  Auto)
  THEN  (With  \mkleeneopen{}m\mkleeneclose{}  (D  3)\mcdot{}  THENA  Auto)
  THEN  D  5
  THEN  (UnhideSqStableHyp  6
              THENA  (Auto  THEN  OnMaybeHyp  11  (\mbackslash{}h.  (FLemma  `i-member-approx`  [h]  THEN  Complete  (Auto))))
              ))

---

Home Index