---

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


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)))
BY
{ ((Assert mdist(d;mtb-seq(mtb;mtb-point-cantor(mtb;x)) j;mtb-seq(mtb;mtb-point-cantor(mtb;y)) 
                                                          m) ≤ (mdist(d;mtb-seq(mtb;mtb-point-cantor(mtb;x)) j;x)
          + mdist(d;x;mtb-seq(mtb;mtb-point-cantor(mtb;y)) m)) BY
          Auto)
   THEN (RWO "-1" 0 THENA Auto)
   THEN Thin (-1)
   THEN (Assert mdist(d;x;mtb-seq(mtb;mtb-point-cantor(mtb;y)) m) ≤ (mdist(d;x;y)
               + mdist(d;y;mtb-seq(mtb;mtb-point-cantor(mtb;y)) m)) BY
               Auto)
   THEN (RWO "-1" 0 THENA Auto)
   THEN Thin (-1)) }

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;x)
+ mdist(d;x;y)
+ mdist(d;y;mtb-seq(mtb;mtb-point-cantor(mtb;y)) m)) ≤ ((r(2)/r(j + 1)) + (r(2)/r(m + 1)))

---

Latex:

---

Latex:

1.  X  :  Type
2.  d  :  metric(X)
3.  mtb  :  m-TB(X;d)
4.  n  :  \mBbbN{}
5.  \mforall{}x:X.  \mforall{}j:\mBbbN{}.    (mdist(d;x;mtb-seq(mtb;mtb-point-cantor(mtb;x))  j)  \mleq{}  (r1/r(j  +  1)))
6.  x  :  X
7.  y  :  X
8.  mdist(d;x;y)  \mleq{}  (r1/r(n  +  1))
9.  j  :  \mBbbN{}n
10.  m  :  \{n...\}
11.  (r1/r(n  +  1))  \mleq{}  (r1/r(j  +  1))
12.  mdist(d;x;y)  \mleq{}  (r1/r(j  +  1))
\mvdash{}  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:
((Assert  mdist(d;mtb-seq(mtb;mtb-point-cantor(mtb;x)) 
                                  j;mtb-seq(mtb;mtb-point-cantor(mtb;y)) 
                                      m)  \mleq{}  (mdist(d;mtb-seq(mtb;mtb-point-cantor(mtb;x))  j;x)
                +  mdist(d;x;mtb-seq(mtb;mtb-point-cantor(mtb;y))  m))  BY
                Auto)
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  Thin  (-1)
  THEN  (Assert  mdist(d;x;mtb-seq(mtb;mtb-point-cantor(mtb;y))  m)  \mleq{}  (mdist(d;x;y)
                          +  mdist(d;y;mtb-seq(mtb;mtb-point-cantor(mtb;y))  m))  BY
                          Auto)
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  Thin  (-1))

---

Home Index