---

Step * 1 1 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. k1 : ℕ+
13. N : ℕ
14. ∀n:ℕ. ((N ≤ n) ⇒ (mdist(c*d;x n;y) ≤ (r1/r(k * k1))))
15. n1 : ℕ
16. N ≤ n1
17. (mdist(d;x n1;y) * c) ≤ (r1/r(k * k1))
⊢ (r1/r(k * k1)) ≤ (c/r(k1))
BY
{ (nRMul ⌜r(k1)⌝ 0⋅ THEN Auto) }

---

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.  k1  :  \mBbbN{}\msupplus{}
13.  N  :  \mBbbN{}
14.  \mforall{}n:\mBbbN{}.  ((N  \mleq{}  n)  {}\mRightarrow{}  (mdist(c*d;x  n;y)  \mleq{}  (r1/r(k  *  k1))))
15.  n1  :  \mBbbN{}
16.  N  \mleq{}  n1
17.  (mdist(d;x  n1;y)  *  c)  \mleq{}  (r1/r(k  *  k1))
\mvdash{}  (r1/r(k  *  k1))  \mleq{}  (c/r(k1))


By

---

Latex:
(nRMul  \mkleeneopen{}r(k1)\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index