---

Step * 1 of Lemma scale-metric-cauchy

.....set predicate..... 
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)
⊢ r0 < (r1/c)
BY
{ (nRMul ⌜c⌝ 0⋅ THEN Auto) }

---

Latex:

---

Latex:
.....set  predicate..... 
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)
\mvdash{}  r0  <  (r1/c)


By

---

Latex:
(nRMul  \mkleeneopen{}c\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index