---

Step * of Lemma scale-metric-converges

No Annotations
∀[X:Type]. ∀[d:metric(X)].  ∀c:{c:ℝ| r0 < c} . ∀x:ℕ ⟶ X. ∀y:X.  (lim n→∞.x n = y ⇐⇒ lim n→∞.x n = y)
BY
{ ((UnivCD THENA Auto)
   THEN (InstLemma `r-archimedean` [⌜c⌝]⋅ THENA Auto)
   THEN (InstLemma `small-reciprocal-real` [⌜c⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN (CaseNat 0 `n'
         THENL [(Eliminate ⌜n⌝⋅ THEN (Assert False BY (DVar `c' THEN Auto)) THEN Auto)
               ; (Auto THEN ParallelLast THEN (D 0 THENA Auto))]
   )) }

1
1. [X] : Type
2. [d] : metric(X)
3. c : {c:ℝ| r0 < c} 
4. x : ℕ ⟶ X
5. y : X
6. n : ℕ
7. r(-n) ≤ c
8. c ≤ r(n)
9. k : ℕ+
10. (r1/r(k)) < c
11. ¬(n = 0 ∈ ℤ)
12. ∀k:ℕ+. (∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (mdist(c*d;x n;y) ≤ (r1/r(k)))))])
13. k1 : ℕ+
⊢ ∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (mdist(d;x n;y) ≤ (r1/r(k1)))))]

2
1. [X] : Type
2. [d] : metric(X)
3. c : {c:ℝ| r0 < c} 
4. x : ℕ ⟶ X
5. y : X
6. n : ℕ
7. r(-n) ≤ c
8. c ≤ r(n)
9. k : ℕ+
10. (r1/r(k)) < c
11. ¬(n = 0 ∈ ℤ)
12. ∀k:ℕ+. (∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (mdist(d;x n;y) ≤ (r1/r(k)))))])
13. k1 : ℕ+
⊢ ∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (mdist(c*d;x n;y) ≤ (r1/r(k1)))))]

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:Type].  \mforall{}[d:metric(X)].
    \mforall{}c:\{c:\mBbbR{}|  r0  <  c\}  .  \mforall{}x:\mBbbN{}  {}\mrightarrow{}  X.  \mforall{}y:X.    (lim  n\mrightarrow{}\minfty{}.x  n  =  y  \mLeftarrow{}{}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.x  n  =  y)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (InstLemma  `r-archimedean`  [\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `small-reciprocal-real`  [\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)
                          ;  (Auto  THEN  ParallelLast  THEN  (D  0  THENA  Auto))]
  ))

---

Home Index