---

Step * 2 1 1 1 1 1 1 of Lemma mtb-cantor-map-onto-common

.....assertion..... 
1. X : Type
2. d : metric(X)
3. cmplt : mcomplete(X with d)
4. mtb : m-TB(X;d)
5. n : ℕ
6. x : X
7. y : X
8. mdist(d;x;y) ≤ (r1/r(n + 1))
9. m-k-regular(d;1;mtb-seq(mtb;mtb-point-cantor(mtb;x)))
10. m-regularize(d;mtb-seq(mtb;mtb-point-cantor(mtb;x))) = mtb-seq(mtb;mtb-point-cantor(mtb;x)) ∈ (ℕ ⟶ X)
11. ∀[s:ℕ ⟶ X]. (λk.(6 * k) ∈ mcauchy(d;n.m-regularize(d;s) n))
12. mtb-cantor(mtb) ⊆r (i:ℕn ⟶ ℕ(fst(mtb)) i)
13. mtb-point-cantor(mtb;x)
= (λi.if i <z n then mtb-point-cantor(mtb;x) i else mtb-point-cantor(mtb;y) i fi )
∈ (i:ℕn ⟶ ℕ(fst(mtb)) i)
14. mtb-cantor-map(d;cmplt;mtb;mtb-point-cantor(mtb;x)) ≡ x
15. m-k-regular(d;1;mtb-seq(mtb;mtb-point-cantor(mtb;y)))
16. ∀[X:Type]. ∀[d:metric(X)]. ∀[s:ℕ ⟶ X].  m-k-regular(d;2;s) supposing m-k-regular(d;1;s)
17. ∀n,m:ℕ.
      (mdist(d;mtb-seq(mtb;mtb-point-cantor(mtb;y)) n;mtb-seq(mtb;mtb-point-cantor(mtb;y)) m) ≤ ((r(2)/r(n + 1))
      + (r(2)/r(m + 1))))
18. ∀n,m:ℕ.
      (mdist(d;mtb-seq(mtb;mtb-point-cantor(mtb;x)) n;mtb-seq(mtb;mtb-point-cantor(mtb;x)) m) ≤ ((r(2)/r(n + 1))
      + (r(2)/r(m + 1))))
19. j : ℕ
20. m : ℕ
⊢ ∀x,y:X.
    ((mdist(d;x;y) ≤ (r1/r(n + 1)))
    ⇒ (∀j:ℕn. ∀m:{n...}.
          (mdist(d;mtb-seq(mtb;mtb-point-cantor(mtb;x)) j;mtb-seq(mtb;mtb-point-cantor(mtb;y)) m) ≤ ((r(2)/r(j + 1))
          + (r(2)/r(m + 1))))))
BY
{ (All Thin
   THEN (Assert ∀x:X. ∀j:ℕ.  (mdist(d;x;mtb-seq(mtb;mtb-point-cantor(mtb;x)) j) ≤ (r1/r(j + 1))) BY
               (All Thin
                THEN (RepeatFor 2 (DVar `mtb') THEN DVar `m1')
                THEN RepUR ``mtb-seq mtb-point-cantor`` 0
                THEN All Reduce
                THEN Auto))
   THEN Auto
   THEN (Assert (r1/r(n + 1)) ≤ (r1/r(j + 1)) BY
               Auto)
   THEN (Assert mdist(d;x;y) ≤ (r1/r(j + 1)) BY
               Auto)) }

1
1. X : Type
2. d : metric(X)
3. mtb : m-TB(X;d)
4. n : ℕ
5. ∀x:X. ∀j:ℕ.  (mdist(d;x;mtb-seq(mtb;mtb-point-cantor(mtb;x)) j) ≤ (r1/r(j + 1)))
6. x : X
7. y : X
8. mdist(d;x;y) ≤ (r1/r(n + 1))
9. j : ℕn
10. m : {n...}
11. (r1/r(n + 1)) ≤ (r1/r(j + 1))
12. mdist(d;x;y) ≤ (r1/r(j + 1))
⊢ mdist(d;mtb-seq(mtb;mtb-point-cantor(mtb;x)) j;mtb-seq(mtb;mtb-point-cantor(mtb;y)) m) ≤ ((r(2)/r(j + 1))
+ (r(2)/r(m + 1)))

---

Latex:

---

Latex:
.....assertion..... 
1.  X  :  Type
2.  d  :  metric(X)
3.  cmplt  :  mcomplete(X  with  d)
4.  mtb  :  m-TB(X;d)
5.  n  :  \mBbbN{}
6.  x  :  X
7.  y  :  X
8.  mdist(d;x;y)  \mleq{}  (r1/r(n  +  1))
9.  m-k-regular(d;1;mtb-seq(mtb;mtb-point-cantor(mtb;x)))
10.  m-regularize(d;mtb-seq(mtb;mtb-point-cantor(mtb;x)))  =  mtb-seq(mtb;mtb-point-cantor(mtb;x))
11.  \mforall{}[s:\mBbbN{}  {}\mrightarrow{}  X].  (\mlambda{}k.(6  *  k)  \mmember{}  mcauchy(d;n.m-regularize(d;s)  n))
12.  mtb-cantor(mtb)  \msubseteq{}r  (i:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}(fst(mtb))  i)
13.  mtb-point-cantor(mtb;x)
=  (\mlambda{}i.if  i  <z  n  then  mtb-point-cantor(mtb;x)  i  else  mtb-point-cantor(mtb;y)  i  fi  )
14.  mtb-cantor-map(d;cmplt;mtb;mtb-point-cantor(mtb;x))  \mequiv{}  x
15.  m-k-regular(d;1;mtb-seq(mtb;mtb-point-cantor(mtb;y)))
16.  \mforall{}[X:Type].  \mforall{}[d:metric(X)].  \mforall{}[s:\mBbbN{}  {}\mrightarrow{}  X].    m-k-regular(d;2;s)  supposing  m-k-regular(d;1;s)
17.  \mforall{}n,m:\mBbbN{}.
            (mdist(d;mtb-seq(mtb;mtb-point-cantor(mtb;y))  n;mtb-seq(mtb;mtb-point-cantor(mtb;y)) 
                                                                                                            m)  \mleq{}  ((r(2)/r(n  +  1))  +  (r(2)/r(m  +  1))))
18.  \mforall{}n,m:\mBbbN{}.
            (mdist(d;mtb-seq(mtb;mtb-point-cantor(mtb;x))  n;mtb-seq(mtb;mtb-point-cantor(mtb;x)) 
                                                                                                            m)  \mleq{}  ((r(2)/r(n  +  1))  +  (r(2)/r(m  +  1))))
19.  j  :  \mBbbN{}
20.  m  :  \mBbbN{}
\mvdash{}  \mforall{}x,y:X.
        ((mdist(d;x;y)  \mleq{}  (r1/r(n  +  1)))
        {}\mRightarrow{}  (\mforall{}j:\mBbbN{}n.  \mforall{}m:\{n...\}.
                    (mdist(d;mtb-seq(mtb;mtb-point-cantor(mtb;x))  j;mtb-seq(mtb;mtb-point-cantor(mtb;y)) 
                                                                                                                    m)  \mleq{}  ((r(2)/r(j  +  1))
                    +  (r(2)/r(m  +  1))))))


By

---

Latex:
(All  Thin
  THEN  (Assert  \mforall{}x:X.  \mforall{}j:\mBbbN{}.    (mdist(d;x;mtb-seq(mtb;mtb-point-cantor(mtb;x))  j)  \mleq{}  (r1/r(j  +  1)))  BY
                          (All  Thin
                            THEN  (RepeatFor  2  (DVar  `mtb')  THEN  DVar  `m1')
                            THEN  RepUR  ``mtb-seq  mtb-point-cantor``  0
                            THEN  All  Reduce
                            THEN  Auto))
  THEN  Auto
  THEN  (Assert  (r1/r(n  +  1))  \mleq{}  (r1/r(j  +  1))  BY
                          Auto)
  THEN  (Assert  mdist(d;x;y)  \mleq{}  (r1/r(j  +  1))  BY
                          Auto))

---

Home Index