---

Step * 1 1 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. m-regularize(d;mtb-seq(mtb;p)) = m-regularize(d;mtb-seq(mtb;q)) ∈ (ℕ(18 * k) + 1 ⟶ X)
13. ∀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))))
14. N1 : ℕ
15. N : ℕ
16. mdist(d;m-regularize(d;mtb-seq(mtb;q)) imax(N1;18 * k);y) ≤ (r1/r(18 * k))
17. mdist(d;m-regularize(d;mtb-seq(mtb;p)) imax(N;18 * k);x) ≤ (r1/r(18 * k))
⊢ mdist(d;x;y) ≤ (r1/r(k))
BY
{ ((Assert mdist(d;m-regularize(d;mtb-seq(mtb;p)) imax(N;18 * k);m-regularize(d;mtb-seq(mtb;p)) (18 * k)) ≤ (r1/r(3
          * k)) BY
          (BackThruSomeHyp THEN Auto))
   THEN (Assert mdist(d;m-regularize(d;mtb-seq(mtb;q)) imax(N1;18 * k);m-regularize(d;mtb-seq(mtb;q)) 
                                                                       (18 * k)) ≤ (r1/r(3 * k)) BY
               (BackThruSomeHyp 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. m-regularize(d;mtb-seq(mtb;p)) = m-regularize(d;mtb-seq(mtb;q)) ∈ (ℕ(18 * k) + 1 ⟶ X)
13. ∀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))))
14. N1 : ℕ
15. N : ℕ
16. mdist(d;m-regularize(d;mtb-seq(mtb;q)) imax(N1;18 * k);y) ≤ (r1/r(18 * k))
17. mdist(d;m-regularize(d;mtb-seq(mtb;p)) imax(N;18 * k);x) ≤ (r1/r(18 * k))
18. mdist(d;m-regularize(d;mtb-seq(mtb;p)) imax(N;18 * k);m-regularize(d;mtb-seq(mtb;p)) (18 * k)) ≤ (r1/r(3 * k))
19. mdist(d;m-regularize(d;mtb-seq(mtb;q)) imax(N1;18 * k);m-regularize(d;mtb-seq(mtb;q)) (18 * k)) ≤ (r1/r(3 * 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.  m-regularize(d;mtb-seq(mtb;p))  =  m-regularize(d;mtb-seq(mtb;q))
13.  \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))))
14.  N1  :  \mBbbN{}
15.  N  :  \mBbbN{}
16.  mdist(d;m-regularize(d;mtb-seq(mtb;q))  imax(N1;18  *  k);y)  \mleq{}  (r1/r(18  *  k))
17.  mdist(d;m-regularize(d;mtb-seq(mtb;p))  imax(N;18  *  k);x)  \mleq{}  (r1/r(18  *  k))
\mvdash{}  mdist(d;x;y)  \mleq{}  (r1/r(k))


By

---

Latex:
((Assert  mdist(d;m-regularize(d;mtb-seq(mtb;p))  imax(N;18  *  k);m-regularize(d;mtb-seq(mtb;p)) 
                                                                                                                              (18  *  k))  \mleq{}  (r1/r(3  *  k))  BY
                (BackThruSomeHyp  THEN  Auto))
  THEN  (Assert  mdist(d;m-regularize(d;mtb-seq(mtb;q))  imax(N1;18  *  k);m-regularize(d;mtb-seq(mtb;q)) 
                                                                                                                                          (18  *  k))  \mleq{}  (r1/r(3  *  k))  BY
                          (BackThruSomeHyp  THEN  Auto))
  )

---

Home Index