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


1. Type
2. metric(X)
3. : ℕ
4. {p:ℝ^k| r0 < ||p||}  ⟶ X
5. X
6. {c:ℝr0 ≤ c} 
7. ∀m:ℕ+. ∀p:{p:ℝ^k| r0 < ||p||} .  ((||p|| ≤ (r(4)/r(m)))  (mdist(d;f p;z) ≤ (c/r(m))))
8. : ℝ^k
9. : ℕ+
10. : ℕ+
11. (c/r(N)) ≤ (r1/r(b))
12. : ℕ
13. realvec-ibs(k;p) n ≠ 1
14. : ℕ
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||
21. ||p|| ≤ (r(4)/r(n 1))
⊢ mdist(d;z;f p) ≤ (r1/r(b))
BY
((InstHyp [⌜1⌝;⌜p⌝7⋅ THENA Auto)
   THEN (RWO "mdist-symm" THENA Auto)
   THEN (RWO "-1" THENA Auto)
   THEN (RWO "11<THENA Auto)) }

1
1. Type
2. metric(X)
3. : ℕ
4. {p:ℝ^k| r0 < ||p||}  ⟶ X
5. X
6. {c:ℝr0 ≤ c} 
7. ∀m:ℕ+. ∀p:{p:ℝ^k| r0 < ||p||} .  ((||p|| ≤ (r(4)/r(m)))  (mdist(d;f p;z) ≤ (c/r(m))))
8. : ℝ^k
9. : ℕ+
10. : ℕ+
11. (c/r(N)) ≤ (r1/r(b))
12. : ℕ
13. realvec-ibs(k;p) n ≠ 1
14. : ℕ
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||
21. ||p|| ≤ (r(4)/r(n 1))
22. mdist(d;f p;z) ≤ (c/r(n 1))
⊢ (c/r(n 1)) ≤ (c/r(N))


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.  N  :  \mBbbN{}\msupplus{}
11.  (c/r(N))  \mleq{}  (r1/r(b))
12.  n  :  \mBbbN{}
13.  realvec-ibs(k;p)  n  \mneq{}  1
14.  m  :  \mBbbN{}
15.  N  \mleq{}  n
16.  N  \mleq{}  m
17.  r0  <  ||p||  \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbN{}.  ((realvec-ibs(k;p)  n)  =  1)
18.  \mforall{}n:\mBbbN{}.  (((realvec-ibs(k;p)  n)  =  0)  {}\mRightarrow{}  (||p||  \mleq{}  (r(4)/r(n  +  1))))
19.  (realvec-ibs(k;p)  m)  =  1
20.  r0  <  ||p||
21.  ||p||  \mleq{}  (r(4)/r(n  +  1))
\mvdash{}  mdist(d;z;f  p)  \mleq{}  (r1/r(b))


By


Latex:
((InstHyp  [\mkleeneopen{}n  +  1\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]  7\mcdot{}  THENA  Auto)
  THEN  (RWO  "mdist-symm"  0  THENA  Auto)
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  (RWO  "11<"  0  THENA  Auto))




Home Index