---

Step * 2 of Lemma scale-metric-cauchy


1. X : Type
2. ∀[d1,d2:metric(X)].  ∀c:{c:ℝ| r0 < c} . (d1 ≤ c*d2 ⇒ (∀x:ℕ ⟶ X. (mcauchy(d2;n.x n) ⇒ mcauchy(d1;n.x n))))
3. d : metric(X)
4. c : {c:ℝ| r0 < c} 
5. x : ℕ ⟶ X
6. mcauchy(c*d;n.x n)
7. x1 : X
8. y : X
⊢ mdist(d;x1;y) ≤ mdist((r1/c)*c*d;x1;y)
BY
{ (RepUR ``mdist scale-metric`` 0 THEN Fold `mdist` 0 THEN nRNorm 0 THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  \mforall{}[d1,d2:metric(X)].
          \mforall{}c:\{c:\mBbbR{}|  r0  <  c\}  .  (d1  \mleq{}  c*d2  {}\mRightarrow{}  (\mforall{}x:\mBbbN{}  {}\mrightarrow{}  X.  (mcauchy(d2;n.x  n)  {}\mRightarrow{}  mcauchy(d1;n.x  n))))
3.  d  :  metric(X)
4.  c  :  \{c:\mBbbR{}|  r0  <  c\} 
5.  x  :  \mBbbN{}  {}\mrightarrow{}  X
6.  mcauchy(c*d;n.x  n)
7.  x1  :  X
8.  y  :  X
\mvdash{}  mdist(d;x1;y)  \mleq{}  mdist((r1/c)*c*d;x1;y)


By

---

Latex:
(RepUR  ``mdist  scale-metric``  0  THEN  Fold  `mdist`  0  THEN  nRNorm  0  THEN  Auto)

---

Home Index