---

Step * 1 of Lemma mtb-cantor-map-continuous


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))
BY
{ ((Assert m-regularize(d;mtb-seq(mtb;p)) = m-regularize(d;mtb-seq(mtb;q)) ∈ (ℕ(18 * k) + 1 ⟶ X) BY
          (EqCDA
           THEN (FunExt THENA Auto)
           THEN RepeatFor 2 (DVar `mtb')
           THEN DVar `m1'
           THEN RepUR ``mtb-seq`` 0
           THEN EqCDA
           THEN (Assert (p x1) = (q x1) ∈ ℤ BY
                       Auto)
           THEN HypSubst' (-1) 0
           THEN Auto))
   THEN (Assert ∀p:mtb-cantor(mtb). ∀k:ℕ+. ∀n,m:ℕ.
                  (((6 * k) ≤ n)
                  ⇒ ((6 * k) ≤ m)
                  ⇒ (mdist(d;m-regularize(d;mtb-seq(mtb;p)) n;m-regularize(d;mtb-seq(mtb;p)) m) ≤ (r1/r(k)))) BY
               ((D 0 THENA Auto)
                THEN (InstLemma `m-regularize-mcauchy` [⌜X⌝;⌜d⌝;⌜mtb-seq(mtb;p1)⌝]⋅ THENA Auto)
                THEN RepUR ``mcauchy`` -1
                THEN (D 0 THENA Auto)
                THEN (Subst' 6 * k1 ~ (λk.(6 * k)) k1 0 THENA Auto)
                THEN (GenConclTerm ⌜λk.(6 * k)⌝⋅ THENA Auto)
                THEN (GenConclTerm ⌜v k1⌝⋅ THENA Auto)
                THEN D -2
                THEN Unhide
                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
14. m-regularize(d;mtb-seq(mtb;p)) = m-regularize(d;mtb-seq(mtb;q)) ∈ (ℕ(18 * k) + 1 ⟶ X)
15. ∀p:mtb-cantor(mtb). ∀k:ℕ+. ∀n,m:ℕ.
      (((6 * k) ≤ n)
      ⇒ ((6 * k) ≤ m)
      ⇒ (mdist(d;m-regularize(d;mtb-seq(mtb;p)) n;m-regularize(d;mtb-seq(mtb;p)) m) ≤ (r1/r(k))))
⊢ mdist(d;x;y) ≤ (r1/r(k))

---

Latex:

---

Latex:

1.  X  :  Type
2.  d  :  metric(X)
3.  cmplt  :  mcomplete(X  with  d)
4.  mtb  :  m-TB(X;d)
5.  k  :  \mBbbN{}\msupplus{}
6.  p  :  mtb-cantor(mtb)
7.  q  :  mtb-cantor(mtb)
8.  \mforall{}i:\mBbbN{}.  ((i  \mleq{}  (18  *  k))  {}\mRightarrow{}  ((p  i)  =  (q  i)))
9.  \mforall{}[s:\mBbbN{}  {}\mrightarrow{}  X].  (\mlambda{}k.(6  *  k)  \mmember{}  mcauchy(d;n.m-regularize(d;s)  n))
10.  x  :  X
11.  y  :  X
12.  lim  n\mrightarrow{}\minfty{}.m-regularize(d;mtb-seq(mtb;q))  n  =  y
13.  lim  n\mrightarrow{}\minfty{}.m-regularize(d;mtb-seq(mtb;p))  n  =  x
\mvdash{}  mdist(d;x;y)  \mleq{}  (r1/r(k))


By

---

Latex:
((Assert  m-regularize(d;mtb-seq(mtb;p))  =  m-regularize(d;mtb-seq(mtb;q))  BY
                (EqCDA
                  THEN  (FunExt  THENA  Auto)
                  THEN  RepeatFor  2  (DVar  `mtb')
                  THEN  DVar  `m1'
                  THEN  RepUR  ``mtb-seq``  0
                  THEN  EqCDA
                  THEN  (Assert  (p  x1)  =  (q  x1)  BY
                                          Auto)
                  THEN  HypSubst'  (-1)  0
                  THEN  Auto))
  THEN  (Assert  \mforall{}p:mtb-cantor(mtb).  \mforall{}k:\mBbbN{}\msupplus{}.  \mforall{}n,m:\mBbbN{}.
                                (((6  *  k)  \mleq{}  n)
                                {}\mRightarrow{}  ((6  *  k)  \mleq{}  m)
                                {}\mRightarrow{}  (mdist(d;m-regularize(d;mtb-seq(mtb;p))  n;m-regularize(d;mtb-seq(mtb;p)) 
                                                                                                                          m)  \mleq{}  (r1/r(k))))  BY
                          ((D  0  THENA  Auto)
                            THEN  (InstLemma  `m-regularize-mcauchy`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}mtb-seq(mtb;p1)\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  RepUR  ``mcauchy``  -1
                            THEN  (D  0  THENA  Auto)
                            THEN  (Subst'  6  *  k1  \msim{}  (\mlambda{}k.(6  *  k))  k1  0  THENA  Auto)
                            THEN  (GenConclTerm  \mkleeneopen{}\mlambda{}k.(6  *  k)\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  (GenConclTerm  \mkleeneopen{}v  k1\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  D  -2
                            THEN  Unhide
                            THEN  Auto))
  )

---

Home Index