---

Step * of Lemma m-regularize-mcauchy

∀[X:Type]. ∀[d:metric(X)]. ∀[s:ℕ ⟶ X].  (λk.(6 * k) ∈ mcauchy(d;n.m-regularize(d;s) n))
BY
{ (Intros
   THEN Unfold `mcauchy` 0
   THEN (MemCD THENA Auto)
   THEN MemTypeCD
   THEN Try (Complete (Auto))
   THEN Assert ⌜∀n:ℕ. ∀m:ℕn.
                  (((6 * k) ≤ n) ⇒ ((6 * k) ≤ m) ⇒ (mdist(d;m-regularize(d;s) n;m-regularize(d;s) m) ≤ (r1/r(k))))⌝
   ⋅) }

1
.....assertion..... 
1. X : Type
2. d : metric(X)
3. s : ℕ ⟶ X
4. k : ℕ+
⊢ ∀n:ℕ. ∀m:ℕn.  (((6 * k) ≤ n) ⇒ ((6 * k) ≤ m) ⇒ (mdist(d;m-regularize(d;s) n;m-regularize(d;s) m) ≤ (r1/r(k))))

2
1. X : Type
2. d : metric(X)
3. s : ℕ ⟶ X
4. k : ℕ+
5. ∀n:ℕ. ∀m:ℕn.  (((6 * k) ≤ n) ⇒ ((6 * k) ≤ m) ⇒ (mdist(d;m-regularize(d;s) n;m-regularize(d;s) m) ≤ (r1/r(k))))
⊢ ∀n,m:ℕ.  (((6 * k) ≤ n) ⇒ ((6 * k) ≤ m) ⇒ (mdist(d;m-regularize(d;s) n;m-regularize(d;s) m) ≤ (r1/r(k))))

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[d:metric(X)].  \mforall{}[s:\mBbbN{}  {}\mrightarrow{}  X].    (\mlambda{}k.(6  *  k)  \mmember{}  mcauchy(d;n.m-regularize(d;s)  n))


By

---

Latex:
(Intros
  THEN  Unfold  `mcauchy`  0
  THEN  (MemCD  THENA  Auto)
  THEN  MemTypeCD
  THEN  Try  (Complete  (Auto))
  THEN  Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  \mforall{}m:\mBbbN{}n.
                                (((6  *  k)  \mleq{}  n)
                                {}\mRightarrow{}  ((6  *  k)  \mleq{}  m)
                                {}\mRightarrow{}  (mdist(d;m-regularize(d;s)  n;m-regularize(d;s)  m)  \mleq{}  (r1/r(k))))\mkleeneclose{}\mcdot{})

---

Home Index