---

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


1. X : Type
2. d : metric(X)
3. k : ℕ
4. λi.r0 ∈ ℝ^k
5. f : {p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)}  ⟶ X
6. z : X
7. c : {c:ℝ| r0 ≤ c} 
8. ∀m:ℕ+. ∀p:{p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)} .
     ((mdist(max-metric(k);p;λi.r0) ≤ (r(4)/r(m))) ⇒ (mdist(d;f p;z) ≤ (c/r(m))))
9. p : ℝ^k
10. b : ℕ+
11. N : ℕ+
12. (c/r(N)) ≤ (r1/r(b))
13. n : ℕ
14. m : ℕ
15. realvec-max-ibs(k;p) m ≠ 1
16. N ≤ n
17. N ≤ m
18. r0 < mdist(max-metric(k);p;λi.r0) ⇐⇒ ∃n:ℕ. ((realvec-max-ibs(k;p) n) = 1 ∈ ℤ)
19. ∀n:ℕ. (((realvec-max-ibs(k;p) n) = 0 ∈ ℤ) ⇒ (mdist(max-metric(k);p;λi.r0) ≤ (r(4)/r(n + 1))))
20. (realvec-max-ibs(k;p) n) = 1 ∈ ℤ
21. r0 < mdist(max-metric(k);p;λi.r0)
22. mdist(max-metric(k);p;λi.r0) ≤ (r(4)/r(m + 1))
⊢ mdist(d;f p;z) ≤ (r1/r(b))
BY
{ ((InstHyp [⌜m + 1⌝;⌜p⌝] 8⋅ THENA Auto) THEN (RWO "-1" 0 THENA Auto) THEN (RWO "12<" 0 THENA Auto)) }

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

---

Latex:

---

Latex:

1.  X  :  Type
2.  d  :  metric(X)
3.  k  :  \mBbbN{}
4.  \mlambda{}i.r0  \mmember{}  \mBbbR{}\^{}k
5.  f  :  \{p:\mBbbR{}\^{}k|  r0  <  mdist(max-metric(k);p;\mlambda{}i.r0)\}    {}\mrightarrow{}  X
6.  z  :  X
7.  c  :  \{c:\mBbbR{}|  r0  \mleq{}  c\} 
8.  \mforall{}m:\mBbbN{}\msupplus{}.  \mforall{}p:\{p:\mBbbR{}\^{}k|  r0  <  mdist(max-metric(k);p;\mlambda{}i.r0)\}  .
          ((mdist(max-metric(k);p;\mlambda{}i.r0)  \mleq{}  (r(4)/r(m)))  {}\mRightarrow{}  (mdist(d;f  p;z)  \mleq{}  (c/r(m))))
9.  p  :  \mBbbR{}\^{}k
10.  b  :  \mBbbN{}\msupplus{}
11.  N  :  \mBbbN{}\msupplus{}
12.  (c/r(N))  \mleq{}  (r1/r(b))
13.  n  :  \mBbbN{}
14.  m  :  \mBbbN{}
15.  realvec-max-ibs(k;p)  m  \mneq{}  1
16.  N  \mleq{}  n
17.  N  \mleq{}  m
18.  r0  <  mdist(max-metric(k);p;\mlambda{}i.r0)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbN{}.  ((realvec-max-ibs(k;p)  n)  =  1)
19.  \mforall{}n:\mBbbN{}.  (((realvec-max-ibs(k;p)  n)  =  0)  {}\mRightarrow{}  (mdist(max-metric(k);p;\mlambda{}i.r0)  \mleq{}  (r(4)/r(n  +  1))))
20.  (realvec-max-ibs(k;p)  n)  =  1
21.  r0  <  mdist(max-metric(k);p;\mlambda{}i.r0)
22.  mdist(max-metric(k);p;\mlambda{}i.r0)  \mleq{}  (r(4)/r(m  +  1))
\mvdash{}  mdist(d;f  p;z)  \mleq{}  (r1/r(b))


By

---

Latex:
((InstHyp  [\mkleeneopen{}m  +  1\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]  8\mcdot{}  THENA  Auto)  THEN  (RWO  "-1"  0  THENA  Auto)  THEN  (RWO  "12<"  0  THENA  Auto))

---

Home Index