---

Step * 2 of Lemma m-regularize-mcauchy


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))))
BY
{ ((UnivCD THENA Auto)
   THEN (Decide ⌜m < n⌝⋅ THEN Auto)
   THEN ((Decide ⌜n < m⌝⋅ THENA Auto)
         THENL [(RWO "mdist-symm" 0 THEN Auto); ((Subst' m ~ n 0 THENA Auto) THEN RWO  "mdist-same" 0 THEN Auto)]
   )) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  d  :  metric(X)
3.  s  :  \mBbbN{}  {}\mrightarrow{}  X
4.  k  :  \mBbbN{}\msupplus{}
5.  \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))))
\mvdash{}  \mforall{}n,m:\mBbbN{}.
        (((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))))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (Decide  \mkleeneopen{}m  <  n\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  ((Decide  \mkleeneopen{}n  <  m\mkleeneclose{}\mcdot{}  THENA  Auto)
              THENL  [(RWO  "mdist-symm"  0  THEN  Auto)
                          ;  ((Subst'  m  \msim{}  n  0  THENA  Auto)  THEN  RWO    "mdist-same"  0  THEN  Auto)]
  ))

---

Home Index