---

Step * of Lemma m-k-regular-mcauchy

∀[X:Type]. ∀[d:metric(X)]. ∀[s:ℕ ⟶ X].  ∀b:ℕ+. (m-k-regular(d;b;s) ⇒ mcauchy(d;n.s n))
BY
{ (Auto
   THEN UnfoldTopAb (-1)
   THEN (D 0 THENA Auto)
   THEN (D 0 With ⌜(2 * b) * k⌝  THENA Auto)
   THEN ParallelOp -2
   THEN ParallelLast
   THEN (RWO "-1" 0 THENA Auto)
   THEN All Thin
   THEN Auto) }

1
1. b : ℕ+
2. k : ℕ+
3. n : ℕ
4. m : ℕ
5. ((2 * b) * k) ≤ n
6. ((2 * b) * k) ≤ m
⊢ ((r(b)/r(n + 1)) + (r(b)/r(m + 1))) ≤ (r1/r(k))

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[d:metric(X)].  \mforall{}[s:\mBbbN{}  {}\mrightarrow{}  X].    \mforall{}b:\mBbbN{}\msupplus{}.  (m-k-regular(d;b;s)  {}\mRightarrow{}  mcauchy(d;n.s  n))


By

---

Latex:
(Auto
  THEN  UnfoldTopAb  (-1)
  THEN  (D  0  THENA  Auto)
  THEN  (D  0  With  \mkleeneopen{}(2  *  b)  *  k\mkleeneclose{}    THENA  Auto)
  THEN  ParallelOp  -2
  THEN  ParallelLast
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  All  Thin
  THEN  Auto)

---

Home Index