---

Step * 1 of Lemma metric-leq-cauchy


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

---

Latex:

---

Latex:

1.  X  :  Type
2.  d1  :  metric(X)
3.  d2  :  metric(X)
4.  c  :  \{c:\mBbbR{}|  r0  <  c\} 
5.  x  :  \mBbbN{}  {}\mrightarrow{}  X
6.  n  :  \mBbbN{}
7.  r(-n)  \mleq{}  c
8.  c  \mleq{}  r(n)
9.  \mneg{}(n  =  0)
10.  k  :  \mBbbN{}\msupplus{}
11.  N  :  \mBbbN{}
12.  \mforall{}n@0,m:\mBbbN{}.    ((N  \mleq{}  n@0)  {}\mRightarrow{}  (N  \mleq{}  m)  {}\mRightarrow{}  (mdist(d2;x  n@0;x  m)  \mleq{}  (r1/r(n  *  k))))
13.  n1  :  \mBbbN{}
14.  \mforall{}m:\mBbbN{}.  ((N  \mleq{}  n1)  {}\mRightarrow{}  (N  \mleq{}  m)  {}\mRightarrow{}  (mdist(d2;x  n1;x  m)  \mleq{}  (r1/r(n  *  k))))
15.  m  :  \mBbbN{}
16.  N  \mleq{}  n1
17.  N  \mleq{}  m
18.  mdist(d2;x  n1;x  m)  \mleq{}  (r1/r(n  *  k))
\mvdash{}  mdist(c*d2;x  n1;x  m)  \mleq{}  (r1/r(k))


By

---

Latex:
((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