---

Step * 1 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))
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))
BY
{ (((RWO "mdist-symm" (-3) THENA Auto) THEN (RWO "mdist-symm" (-4) THENA Auto))
   THEN (Assert mdist(d;x;m-regularize(d;mtb-seq(mtb;p)) (18 * k)) ≤ (r(7)/r(18 * k)) BY
               ((Assert mdist(d;x;m-regularize(d;mtb-seq(mtb;p)) (18 * k)) ≤ (mdist(d;x;m-regularize(d;mtb-seq(mtb;p)) 
                                                                                        imax(N;18 * k))
                       + mdist(d;m-regularize(d;mtb-seq(mtb;p)) imax(N;18 * k);m-regularize(d;mtb-seq(mtb;p)) 
                                                                               (18 * k))) BY
                       Auto)
                THEN (RWO "-3 -4" (-1) THENA Auto)
                THEN (Assert ((r1/r(18 * k)) + (r1/r(3 * k))) = (r(7)/r(18 * k)) BY
                            (RWO "radd-int-fractions" 0 THEN Auto))
                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;y;m-regularize(d;mtb-seq(mtb;q)) imax(N1;18 * k)) ≤ (r1/r(18 * k))
17. mdist(d;x;m-regularize(d;mtb-seq(mtb;p)) imax(N;18 * k)) ≤ (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))
20. mdist(d;x;m-regularize(d;mtb-seq(mtb;p)) (18 * k)) ≤ (r(7)/r(18 * 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))
18.  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))
19.  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))
\mvdash{}  mdist(d;x;y)  \mleq{}  (r1/r(k))


By

---

Latex:
(((RWO  "mdist-symm"  (-3)  THENA  Auto)  THEN  (RWO  "mdist-symm"  (-4)  THENA  Auto))
  THEN  (Assert  mdist(d;x;m-regularize(d;mtb-seq(mtb;p))  (18  *  k))  \mleq{}  (r(7)/r(18  *  k))  BY
                          ((Assert  mdist(d;x;m-regularize(d;mtb-seq(mtb;p)) 
                                                                (18  *  k))  \mleq{}  (mdist(d;x;m-regularize(d;mtb-seq(mtb;p)) 
                                                                                                              imax(N;18  *  k))
                                          +  mdist(d;m-regularize(d;mtb-seq(mtb;p)) 
                                                              imax(N;18  *  k);m-regularize(d;mtb-seq(mtb;p))  (18  *  k)))  BY
                                          Auto)
                            THEN  (RWO  "-3  -4"  (-1)  THENA  Auto)
                            THEN  (Assert  ((r1/r(18  *  k))  +  (r1/r(3  *  k)))  =  (r(7)/r(18  *  k))  BY
                                                    (RWO  "radd-int-fractions"  0  THEN  Auto))
                            THEN  Auto))
  )

---

Home Index