---

Step * 1 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) * c) ≤ ((c/r(n))/r(k))
⊢ (mdist(d2;x n1;x m) * c) ≤ (r1/r(k))
BY
{ ((RWO "-1" 0 THENA Auto) THEN (nRMul ⌜r(k)⌝ 0⋅ THENA Auto) THEN nRMul ⌜r(n)⌝ 0⋅ THEN Auto) }

---

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)  *  c)  \mleq{}  ((c/r(n))/r(k))
\mvdash{}  (mdist(d2;x  n1;x  m)  *  c)  \mleq{}  (r1/r(k))


By

---

Latex:
((RWO  "-1"  0  THENA  Auto)  THEN  (nRMul  \mkleeneopen{}r(k)\mkleeneclose{}  0\mcdot{}  THENA  Auto)  THEN  nRMul  \mkleeneopen{}r(n)\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index