---

Step * 2 of Lemma scale-metric-converges


1. [X] : Type
2. [d] : metric(X)
3. c : {c:ℝ| r0 < c} 
4. x : ℕ ⟶ X
5. y : X
6. n : ℕ
7. r(-n) ≤ c
8. c ≤ r(n)
9. k : ℕ+
10. (r1/r(k)) < c
11. ¬(n = 0 ∈ ℤ)
12. ∀k:ℕ+. (∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (mdist(d;x n;y) ≤ (r1/r(k)))))])
13. k1 : ℕ+
⊢ ∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (mdist(c*d;x n;y) ≤ (r1/r(k1)))))]
BY
{ ((D -2 With ⌜n * k1⌝  THENA Auto)
   THEN RepeatFor 3 (ParallelLast)
   THEN (RepUR ``mdist scale-metric`` 0 THEN Fold `mdist` 0)
   THEN (nRMul ⌜c⌝ (-1)⋅ THENA Auto)
   THEN (nRNorm 0 THENA Auto)) }

1
1. X : Type
2. d : metric(X)
3. c : {c:ℝ| r0 < c} 
4. x : ℕ ⟶ X
5. y : X
6. n : ℕ
7. r(-n) ≤ c
8. c ≤ r(n)
9. k : ℕ+
10. (r1/r(k)) < c
11. ¬(n = 0 ∈ ℤ)
12. k1 : ℕ+
13. N : ℕ
14. ∀n@0:ℕ. ((N ≤ n@0) ⇒ (mdist(d;x n@0;y) ≤ (r1/r(n * k1))))
15. n1 : ℕ
16. N ≤ n1
17. (mdist(d;x n1;y) * c) ≤ ((c/r(n))/r(k1))
⊢ (mdist(d;x n1;y) * c) ≤ (r1/r(k1))

---

Latex:

---

Latex:

1.  [X]  :  Type
2.  [d]  :  metric(X)
3.  c  :  \{c:\mBbbR{}|  r0  <  c\} 
4.  x  :  \mBbbN{}  {}\mrightarrow{}  X
5.  y  :  X
6.  n  :  \mBbbN{}
7.  r(-n)  \mleq{}  c
8.  c  \mleq{}  r(n)
9.  k  :  \mBbbN{}\msupplus{}
10.  (r1/r(k))  <  c
11.  \mneg{}(n  =  0)
12.  \mforall{}k:\mBbbN{}\msupplus{}.  (\mexists{}N:\mBbbN{}  [(\mforall{}n:\mBbbN{}.  ((N  \mleq{}  n)  {}\mRightarrow{}  (mdist(d;x  n;y)  \mleq{}  (r1/r(k)))))])
13.  k1  :  \mBbbN{}\msupplus{}
\mvdash{}  \mexists{}N:\mBbbN{}  [(\mforall{}n:\mBbbN{}.  ((N  \mleq{}  n)  {}\mRightarrow{}  (mdist(c*d;x  n;y)  \mleq{}  (r1/r(k1)))))]


By

---

Latex:
((D  -2  With  \mkleeneopen{}n  *  k1\mkleeneclose{}    THENA  Auto)
  THEN  RepeatFor  3  (ParallelLast)
  THEN  (RepUR  ``mdist  scale-metric``  0  THEN  Fold  `mdist`  0)
  THEN  (nRMul  \mkleeneopen{}c\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  (nRNorm  0  THENA  Auto))

---

Home Index