---

Step * of Lemma mtb-cantor-map-continuous

No Annotations
∀[X:Type]. ∀[d:metric(X)]. ∀[cmplt:mcomplete(X with d)]. ∀[mtb:m-TB(X;d)]. ∀[k:ℕ+]. ∀[p,q:mtb-cantor(mtb)].
  mdist(d;mtb-cantor-map(d;cmplt;mtb;p);mtb-cantor-map(d;cmplt;mtb;q)) ≤ (r1/r(k)) 
  supposing ∀i:ℕ. ((i ≤ (18 * k)) ⇒ ((p i) = (q i) ∈ ℤ))
BY
{ (Auto
   THEN Try ((RepeatFor 2 (DVar `mtb') THEN Reduce 0 THEN RepeatFor 2 (MemCD)))
   THEN (InstLemma `m-regularize-mcauchy` [⌜X⌝;⌜d⌝]⋅ THENA Auto)
   THEN RepUR ``mtb-cantor-map`` 0
   THEN (InstLemma `converges-to-cauchy-mlimit` [⌜X⌝;⌜d⌝;⌜cmplt⌝;⌜m-regularize(d;mtb-seq(mtb;p))⌝;⌜λk.(6 * k)⌝]⋅
         THENA Auto
         )
   THEN MoveToConcl (-1)
   THEN (GenConclAtAddr [1;3] THENA Auto)
   THEN Thin (-1)
   THEN RenameVar `x' (-1)
   THEN (InstLemma `converges-to-cauchy-mlimit` [⌜X⌝;⌜d⌝;⌜cmplt⌝;⌜m-regularize(d;mtb-seq(mtb;q))⌝;⌜λk.(6 * k)⌝]⋅
         THENA Auto
         )
   THEN MoveToConcl (-1)
   THEN (GenConclAtAddr [1;3] THENA Auto)
   THEN Thin (-1)
   THEN RenameVar `y' (-1)
   THEN Auto) }

1
1. X : Type
2. d : metric(X)
3. cmplt : mcomplete(X with d)
4. mtb : m-TB(X;d)
5. k : ℕ+
6. p : mtb-cantor(mtb)
7. q : mtb-cantor(mtb)
8. ∀i:ℕ. ((i ≤ (18 * k)) ⇒ ((p i) = (q i) ∈ ℤ))
9. ∀[s:ℕ ⟶ X]. (λk.(6 * k) ∈ mcauchy(d;n.m-regularize(d;s) n))
10. x : X
11. y : X
12. lim n→∞.m-regularize(d;mtb-seq(mtb;q)) n = y
13. lim n→∞.m-regularize(d;mtb-seq(mtb;p)) n = x
⊢ mdist(d;x;y) ≤ (r1/r(k))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:Type].  \mforall{}[d:metric(X)].  \mforall{}[cmplt:mcomplete(X  with  d)].  \mforall{}[mtb:m-TB(X;d)].  \mforall{}[k:\mBbbN{}\msupplus{}].
\mforall{}[p,q:mtb-cantor(mtb)].
    mdist(d;mtb-cantor-map(d;cmplt;mtb;p);mtb-cantor-map(d;cmplt;mtb;q))  \mleq{}  (r1/r(k)) 
    supposing  \mforall{}i:\mBbbN{}.  ((i  \mleq{}  (18  *  k))  {}\mRightarrow{}  ((p  i)  =  (q  i)))


By

---

Latex:
(Auto
  THEN  Try  ((RepeatFor  2  (DVar  `mtb')  THEN  Reduce  0  THEN  RepeatFor  2  (MemCD)))
  THEN  (InstLemma  `m-regularize-mcauchy`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepUR  ``mtb-cantor-map``  0
  THEN  (InstLemma  `converges-to-cauchy-mlimit`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}cmplt\mkleeneclose{};\mkleeneopen{}m-regularize(d;mtb-seq(mtb;p))\mkleeneclose{};
              \mkleeneopen{}\mlambda{}k.(6  *  k)\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  MoveToConcl  (-1)
  THEN  (GenConclAtAddr  [1;3]  THENA  Auto)
  THEN  Thin  (-1)
  THEN  RenameVar  `x'  (-1)
  THEN  (InstLemma  `converges-to-cauchy-mlimit`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}cmplt\mkleeneclose{};\mkleeneopen{}m-regularize(d;mtb-seq(mtb;q))\mkleeneclose{};
              \mkleeneopen{}\mlambda{}k.(6  *  k)\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  MoveToConcl  (-1)
  THEN  (GenConclAtAddr  [1;3]  THENA  Auto)
  THEN  Thin  (-1)
  THEN  RenameVar  `y'  (-1)
  THEN  Auto)

---

Home Index