---

Step * of Lemma m-k-regular-monotone

∀[n,k:ℕ].  ∀[X:Type]. ∀[d:metric(X)]. ∀[s:ℕ ⟶ X].  m-k-regular(d;k;s) supposing m-k-regular(d;n;s) supposing n ≤ k
BY
{ (Auto THEN RepeatFor 3 (ParallelLast) THEN (RWO  "-1" 0 THENA Auto)) }

1
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(n1 + 1)) + (r(n)/r(m + 1))) ≤ ((r(k)/r(n1 + 1)) + (r(k)/r(m + 1)))

---

Latex:

---

Latex:
\mforall{}[n,k:\mBbbN{}].
    \mforall{}[X:Type].  \mforall{}[d:metric(X)].  \mforall{}[s:\mBbbN{}  {}\mrightarrow{}  X].    m-k-regular(d;k;s)  supposing  m-k-regular(d;n;s) 
    supposing  n  \mleq{}  k


By

---

Latex:
(Auto  THEN  RepeatFor  3  (ParallelLast)  THEN  (RWO    "-1"  0  THENA  Auto))

---

Home Index