---

Step * of Lemma mtb-seq-mtb-point-cantor-mconverges-to

∀[X:Type]. ∀d:metric(X). ∀mtb:m-TB(X;d). ∀x:X.  lim n→∞.mtb-seq(mtb;mtb-point-cantor(mtb;x)) n = x
BY
{ (Auto
   THEN (RepeatFor 2 (DVar `mtb') THEN DVar `m1')
   THEN RepUR ``mtb-point-cantor mtb-seq`` 0
   THEN All Reduce
   THEN (D 0 THENA Auto)
   THEN D 0 With ⌜k⌝ 
   THEN Auto
   THEN (RWO "mdist-symm" 0 THENA Auto)
   THEN RWO "-5" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}d:metric(X).  \mforall{}mtb:m-TB(X;d).  \mforall{}x:X.    lim  n\mrightarrow{}\minfty{}.mtb-seq(mtb;mtb-point-cantor(mtb;x))  n  =  x


By

---

Latex:
(Auto
  THEN  (RepeatFor  2  (DVar  `mtb')  THEN  DVar  `m1')
  THEN  RepUR  ``mtb-point-cantor  mtb-seq``  0
  THEN  All  Reduce
  THEN  (D  0  THENA  Auto)
  THEN  D  0  With  \mkleeneopen{}k\mkleeneclose{} 
  THEN  Auto
  THEN  (RWO  "mdist-symm"  0  THENA  Auto)
  THEN  RWO  "-5"  0
  THEN  Auto)

---

Home Index