---

Step * 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. 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))
BY
{ (RepeatFor 2 ((D -4 With ⌜18 * k⌝  THENA Auto))
   THEN ExRepD
   THEN ((InstHyp [⌜imax(N1;18 * k)⌝] (-3)⋅ THENA Auto) THEN Thin (-4))
   THEN (InstHyp [⌜imax(N;18 * k)⌝] (-2)⋅ THENA Auto)
   THEN Thin (-3)) }

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))
⊢ 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
14.  m-regularize(d;mtb-seq(mtb;p))  =  m-regularize(d;mtb-seq(mtb;q))
15.  \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))))
\mvdash{}  mdist(d;x;y)  \mleq{}  (r1/r(k))


By

---

Latex:
(RepeatFor  2  ((D  -4  With  \mkleeneopen{}18  *  k\mkleeneclose{}    THENA  Auto))
  THEN  ExRepD
  THEN  ((InstHyp  [\mkleeneopen{}imax(N1;18  *  k)\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)  THEN  Thin  (-4))
  THEN  (InstHyp  [\mkleeneopen{}imax(N;18  *  k)\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  Thin  (-3))

---

Home Index