---

Step * 1 2 of Lemma remove-singularity-seq-mcauchy


1. [X] : Type
2. [d] : metric(X)
3. [k] : ℕ
4. [f] : {p:ℝ^k| r0 < ||p||}  ⟶ X
5. [z] : X
6. c : {c:ℝ| r0 ≤ c} 
7. ∀m:ℕ+. ∀p:{p:ℝ^k| r0 < ||p||} .  ((||p|| ≤ (r(4)/r(m))) ⇒ (mdist(d;f p;z) ≤ (c/r(m))))
8. [p] : ℝ^k
9. b : ℕ+
10. ∃N:ℕ+. ((c/r(N)) ≤ (r1/r(b)))
⊢ ∃N:ℕ [(∀n,m:ℕ.
           ((N ≤ n)
           ⇒ (N ≤ m)
           ⇒ (mdist(d;remove-singularity-seq(k;p;f;z) n;remove-singularity-seq(k;p;f;z) m) ≤ (r1/r(b)))))]
BY
{ (((ParallelLast THEN Auto) THEN RepUR ``remove-singularity-seq`` 0)
   THEN (InstLemma `realvec-ibs-property` [⌜k⌝;⌜p⌝]⋅ THENA Auto)
   THEN D -1
   THEN RepeatFor 2 (AutoSplit)
   THEN ((RWO "mdist-same" 0 THEN Auto) ORELSE (Assert r0 < ||p|| BY (BackThruSomeHyp THEN 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} 
7. ∀m:ℕ+. ∀p:{p:ℝ^k| r0 < ||p||} .  ((||p|| ≤ (r(4)/r(m))) ⇒ (mdist(d;f p;z) ≤ (c/r(m))))
8. p : ℝ^k
9. b : ℕ+
10. N : ℕ+
11. (c/r(N)) ≤ (r1/r(b))
12. n : ℕ
13. m : ℕ
14. realvec-ibs(k;p) m ≠ 1
15. N ≤ n
16. N ≤ m
17. r0 < ||p|| ⇐⇒ ∃n:ℕ. ((realvec-ibs(k;p) n) = 1 ∈ ℤ)
18. ∀n:ℕ. (((realvec-ibs(k;p) n) = 0 ∈ ℤ) ⇒ (||p|| ≤ (r(4)/r(n + 1))))
19. (realvec-ibs(k;p) n) = 1 ∈ ℤ
20. r0 < ||p||
⊢ mdist(d;f p;z) ≤ (r1/r(b))

2
1. X : Type
2. d : metric(X)
3. k : ℕ
4. f : {p:ℝ^k| r0 < ||p||}  ⟶ X
5. z : X
6. c : {c:ℝ| r0 ≤ c} 
7. ∀m:ℕ+. ∀p:{p:ℝ^k| r0 < ||p||} .  ((||p|| ≤ (r(4)/r(m))) ⇒ (mdist(d;f p;z) ≤ (c/r(m))))
8. p : ℝ^k
9. b : ℕ+
10. N : ℕ+
11. (c/r(N)) ≤ (r1/r(b))
12. n : ℕ
13. realvec-ibs(k;p) n ≠ 1
14. m : ℕ
15. N ≤ n
16. N ≤ m
17. r0 < ||p|| ⇐⇒ ∃n:ℕ. ((realvec-ibs(k;p) n) = 1 ∈ ℤ)
18. ∀n:ℕ. (((realvec-ibs(k;p) n) = 0 ∈ ℤ) ⇒ (||p|| ≤ (r(4)/r(n + 1))))
19. (realvec-ibs(k;p) m) = 1 ∈ ℤ
20. r0 < ||p||
⊢ mdist(d;z;f p) ≤ (r1/r(b))

---

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.  c  :  \{c:\mBbbR{}|  r0  \mleq{}  c\} 
7.  \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))))
8.  [p]  :  \mBbbR{}\^{}k
9.  b  :  \mBbbN{}\msupplus{}
10.  \mexists{}N:\mBbbN{}\msupplus{}.  ((c/r(N))  \mleq{}  (r1/r(b)))
\mvdash{}  \mexists{}N:\mBbbN{}  [(\mforall{}n,m:\mBbbN{}.
                      ((N  \mleq{}  n)
                      {}\mRightarrow{}  (N  \mleq{}  m)
                      {}\mRightarrow{}  (mdist(d;remove-singularity-seq(k;p;f;z)  n;remove-singularity-seq(k;p;f;z) 
                                                                                                                  m)  \mleq{}  (r1/r(b)))))]


By

---

Latex:
(((ParallelLast  THEN  Auto)  THEN  RepUR  ``remove-singularity-seq``  0)
  THEN  (InstLemma  `realvec-ibs-property`  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  RepeatFor  2  (AutoSplit)
  THEN  ((RWO  "mdist-same"  0  THEN  Auto)  ORELSE  (Assert  r0  <  ||p||  BY  (BackThruSomeHyp  THEN  Auto))))

---

Home Index