---

Step * 1 2 of Lemma m-k-regular-monotone


1. n : ℕ
2. k : ℕ
3. n ≤ k
4. X : Type
5. d : metric(X)
6. s : ℕ ⟶ X
7. ∀n@0,m:ℕ.  (mdist(d;s n@0;s m) ≤ ((r(n)/r(n@0 + 1)) + (r(n)/r(m + 1))))
8. n1 : ℕ
9. ∀m:ℕ. (mdist(d;s n1;s m) ≤ ((r(n)/r(n1 + 1)) + (r(n)/r(m + 1))))
10. m : ℕ
11. mdist(d;s n1;s m) ≤ ((r(n)/r(n1 + 1)) + (r(n)/r(m + 1)))
⊢ (r(n)/r(m + 1)) ≤ (r(k)/r(m + 1))
BY
{ (nRMul ⌜r(m + 1)⌝ 0⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  k  :  \mBbbN{}
3.  n  \mleq{}  k
4.  X  :  Type
5.  d  :  metric(X)
6.  s  :  \mBbbN{}  {}\mrightarrow{}  X
7.  \mforall{}n@0,m:\mBbbN{}.    (mdist(d;s  n@0;s  m)  \mleq{}  ((r(n)/r(n@0  +  1))  +  (r(n)/r(m  +  1))))
8.  n1  :  \mBbbN{}
9.  \mforall{}m:\mBbbN{}.  (mdist(d;s  n1;s  m)  \mleq{}  ((r(n)/r(n1  +  1))  +  (r(n)/r(m  +  1))))
10.  m  :  \mBbbN{}
11.  mdist(d;s  n1;s  m)  \mleq{}  ((r(n)/r(n1  +  1))  +  (r(n)/r(m  +  1)))
\mvdash{}  (r(n)/r(m  +  1))  \mleq{}  (r(k)/r(m  +  1))


By

---

Latex:
(nRMul  \mkleeneopen{}r(m  +  1)\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index