---

Step * 2 of Lemma remove-singularity


1. X : Type
2. d : metric(X)
3. k : ℕ
4. f : {p:ℝ^k| r0 < ||p||}  ⟶ X
5. z : X
6. ∃c:{c:ℝ| r0 ≤ c} . ∀m:ℕ+. ∀p:{p:ℝ^k| r0 < ||p||} .  ((||p|| ≤ (r(4)/r(m))) ⇒ (mdist(d;f p;z) ≤ (c/r(m))))
7. cau : ∀[p:ℝ^k]. mcauchy(d;n.remove-singularity-seq(k;p;f;z) n)
8. cmplt : mcomplete(X with d)
9. ∀p:ℝ^k. (req-vec(k;p;λi.r0) ⇒ cauchy-mlimit(cmplt;remove-singularity-seq(k;p;f;z);cau) ≡ z)
10. p : {p:ℝ^k| r0 < ||p||} 
⊢ lim n→∞.remove-singularity-seq(k;p;f;z) n = f p
BY
{ ((Assert r0 < ||p|| BY
          Auto)
   THEN InstLemma `realvec-ibs-property` [⌜k⌝;⌜p⌝]⋅
   THEN Auto
   THEN D -1
   THEN (InstLemma `ibs-property` [⌜realvec-ibs(k;p)⌝;⌜n⌝]⋅ THENA Auto)) }

1
1. X : Type
2. d : metric(X)
3. k : ℕ
4. f : {p:ℝ^k| r0 < ||p||}  ⟶ X
5. z : X
6. ∃c:{c:ℝ| r0 ≤ c} . ∀m:ℕ+. ∀p:{p:ℝ^k| r0 < ||p||} .  ((||p|| ≤ (r(4)/r(m))) ⇒ (mdist(d;f p;z) ≤ (c/r(m))))
7. cau : ∀[p:ℝ^k]. mcauchy(d;n.remove-singularity-seq(k;p;f;z) n)
8. cmplt : mcomplete(X with d)
9. ∀p:ℝ^k. (req-vec(k;p;λi.r0) ⇒ cauchy-mlimit(cmplt;remove-singularity-seq(k;p;f;z);cau) ≡ z)
10. p : {p:ℝ^k| r0 < ||p||} 
11. r0 < ||p||
12. (r0 < ||p||) ⇐ ∃n:ℕ. ((realvec-ibs(k;p) n) = 1 ∈ ℤ)
13. ∀n:ℕ. (((realvec-ibs(k;p) n) = 0 ∈ ℤ) ⇒ (||p|| ≤ (r(4)/r(n + 1))))
14. n : ℕ
15. (realvec-ibs(k;p) n) = 1 ∈ ℤ
16. ∀[n@0:ℕ]. (realvec-ibs(k;p) n@0) = 1 ∈ ℤ supposing n ≤ n@0
⊢ lim n→∞.remove-singularity-seq(k;p;f;z) n = f p

---

Latex:

---

Latex:

1.  X  :  Type
2.  d  :  metric(X)
3.  k  :  \mBbbN{}
4.  f  :  \{p:\mBbbR{}\^{}k|  r0  <  ||p||\}    {}\mrightarrow{}  X
5.  z  :  X
6.  \mexists{}c:\{c:\mBbbR{}|  r0  \mleq{}  c\} 
        \mforall{}m:\mBbbN{}\msupplus{}.  \mforall{}p:\{p:\mBbbR{}\^{}k|  r0  <  ||p||\}  .    ((||p||  \mleq{}  (r(4)/r(m)))  {}\mRightarrow{}  (mdist(d;f  p;z)  \mleq{}  (c/r(m))))
7.  cau  :  \mforall{}[p:\mBbbR{}\^{}k].  mcauchy(d;n.remove-singularity-seq(k;p;f;z)  n)
8.  cmplt  :  mcomplete(X  with  d)
9.  \mforall{}p:\mBbbR{}\^{}k.  (req-vec(k;p;\mlambda{}i.r0)  {}\mRightarrow{}  cauchy-mlimit(cmplt;remove-singularity-seq(k;p;f;z);cau)  \mequiv{}  z)
10.  p  :  \{p:\mBbbR{}\^{}k|  r0  <  ||p||\} 
\mvdash{}  lim  n\mrightarrow{}\minfty{}.remove-singularity-seq(k;p;f;z)  n  =  f  p


By

---

Latex:
((Assert  r0  <  ||p||  BY
                Auto)
  THEN  InstLemma  `realvec-ibs-property`  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  D  -1
  THEN  (InstLemma  `ibs-property`  [\mkleeneopen{}realvec-ibs(k;p)\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index