---

Step * of Lemma metric-leq-cauchy

No Annotations
∀[X:Type]. ∀[d1,d2:metric(X)].  ∀c:{c:ℝ| r0 < c} . (d1 ≤ c*d2 ⇒ (∀x:ℕ ⟶ X. (mcauchy(d2;n.x n) ⇒ mcauchy(d1;n.x n))))
BY
{ ((UnivCD THENA Auto)
   THEN (InstLemma `r-archimedean` [⌜c⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN (CaseNat 0 `n'
         THENL [(Eliminate ⌜n⌝⋅ THEN (Assert False BY (DVar `c' THEN Auto)) THEN Auto)
               ; (ParallelOp 7
                  THEN (D 0 THENA Auto)
                  THEN (D 7 With ⌜n * k⌝  THENA Auto)
                  THEN RepeatFor 5 (ParallelLast)
                  THEN (D 5 With ⌜x n1⌝  THENA Auto)
                  THEN (D -1 With ⌜x m⌝  THENA Auto)
                  THEN (RWO "-1" 0 THENA Auto)
                  THEN Thin (-1))]
   )) }

1
1. X : Type
2. d1 : metric(X)
3. d2 : metric(X)
4. c : {c:ℝ| r0 < c} 
5. x : ℕ ⟶ X
6. n : ℕ
7. r(-n) ≤ c
8. c ≤ r(n)
9. ¬(n = 0 ∈ ℤ)
10. k : ℕ+
11. N : ℕ
12. ∀n@0,m:ℕ.  ((N ≤ n@0) ⇒ (N ≤ m) ⇒ (mdist(d2;x n@0;x m) ≤ (r1/r(n * k))))
13. n1 : ℕ
14. ∀m:ℕ. ((N ≤ n1) ⇒ (N ≤ m) ⇒ (mdist(d2;x n1;x m) ≤ (r1/r(n * k))))
15. m : ℕ
16. N ≤ n1
17. N ≤ m
18. mdist(d2;x n1;x m) ≤ (r1/r(n * k))
⊢ mdist(c*d2;x n1;x m) ≤ (r1/r(k))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:Type].  \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))))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (InstLemma  `r-archimedean`  [\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (CaseNat  0  `n'
              THENL  [(Eliminate  \mkleeneopen{}n\mkleeneclose{}\mcdot{}  THEN  (Assert  False  BY  (DVar  `c'  THEN  Auto))  THEN  Auto)
                          ;  (ParallelOp  7
                                THEN  (D  0  THENA  Auto)
                                THEN  (D  7  With  \mkleeneopen{}n  *  k\mkleeneclose{}    THENA  Auto)
                                THEN  RepeatFor  5  (ParallelLast)
                                THEN  (D  5  With  \mkleeneopen{}x  n1\mkleeneclose{}    THENA  Auto)
                                THEN  (D  -1  With  \mkleeneopen{}x  m\mkleeneclose{}    THENA  Auto)
                                THEN  (RWO  "-1"  0  THENA  Auto)
                                THEN  Thin  (-1))]
  ))

---

Home Index