---

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


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-regularize(d;mtb-seq(mtb;λi.if i <z n then mtb-point-cantor(mtb;x) i else mtb-point-cantor(mtb;y) i fi ))
= mtb-seq(mtb;λi.if i <z n then mtb-point-cantor(mtb;x) i else mtb-point-cantor(mtb;y) i fi )
∈ (ℕ ⟶ X)
16. ∀k:ℕ+. (∃N:ℕ [(∀n1:ℕ. ((N ≤ n1) ⇒ (mdist(d;mtb-seq(mtb;mtb-point-cantor(mtb;y)) n1;y) ≤ (r1/r(k)))))])
17. k : ℕ+
18. N : ℕ
19. ∀n1:ℕ. ((N ≤ n1) ⇒ (mdist(d;mtb-seq(mtb;mtb-point-cantor(mtb;y)) n1;y) ≤ (r1/r(k))))
⊢ ∀n1:ℕ
    ((imax(n;N) ≤ n1)
    ⇒ (mdist(d;mtb-seq(mtb;λi.if i <z n then mtb-point-cantor(mtb;x) i else mtb-point-cantor(mtb;y) i fi ) 
                n1;y) ≤ (r1/r(k))))
BY
{ RepeatFor 2 ((ParallelLast THENA ((Assert N ≤ imax(n;N) BY Auto) THEN Auto))) }

1
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-regularize(d;mtb-seq(mtb;λi.if i <z n then mtb-point-cantor(mtb;x) i else mtb-point-cantor(mtb;y) i fi ))
= mtb-seq(mtb;λi.if i <z n then mtb-point-cantor(mtb;x) i else mtb-point-cantor(mtb;y) i fi )
∈ (ℕ ⟶ X)
16. ∀k:ℕ+. (∃N:ℕ [(∀n1:ℕ. ((N ≤ n1) ⇒ (mdist(d;mtb-seq(mtb;mtb-point-cantor(mtb;y)) n1;y) ≤ (r1/r(k)))))])
17. k : ℕ+
18. N : ℕ
19. ∀n1:ℕ. ((N ≤ n1) ⇒ (mdist(d;mtb-seq(mtb;mtb-point-cantor(mtb;y)) n1;y) ≤ (r1/r(k))))
20. n1 : ℕ
21. imax(n;N) ≤ n1
22. mdist(d;mtb-seq(mtb;mtb-point-cantor(mtb;y)) n1;y) ≤ (r1/r(k))
⊢ mdist(d;mtb-seq(mtb;λi.if i <z n then mtb-point-cantor(mtb;x) i else mtb-point-cantor(mtb;y) i fi ) n1;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.  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-regularize(d;mtb-seq(mtb;\mlambda{}i.if  i  <z  n
                                                                    then  mtb-point-cantor(mtb;x)  i
                                                                    else  mtb-point-cantor(mtb;y)  i
                                                                    fi  ))
=  mtb-seq(mtb;\mlambda{}i.if  i  <z  n  then  mtb-point-cantor(mtb;x)  i  else  mtb-point-cantor(mtb;y)  i  fi  )
16.  \mforall{}k:\mBbbN{}\msupplus{}
            (\mexists{}N:\mBbbN{}  [(\mforall{}n1:\mBbbN{}
                                ((N  \mleq{}  n1)  {}\mRightarrow{}  (mdist(d;mtb-seq(mtb;mtb-point-cantor(mtb;y))  n1;y)  \mleq{}  (r1/r(k)))))])
17.  k  :  \mBbbN{}\msupplus{}
18.  N  :  \mBbbN{}
19.  \mforall{}n1:\mBbbN{}.  ((N  \mleq{}  n1)  {}\mRightarrow{}  (mdist(d;mtb-seq(mtb;mtb-point-cantor(mtb;y))  n1;y)  \mleq{}  (r1/r(k))))
\mvdash{}  \mforall{}n1:\mBbbN{}
        ((imax(n;N)  \mleq{}  n1)
        {}\mRightarrow{}  (mdist(d;mtb-seq(mtb;\mlambda{}i.if  i  <z  n
                                                              then  mtb-point-cantor(mtb;x)  i
                                                              else  mtb-point-cantor(mtb;y)  i
                                                              fi  ) 
                                n1;y)  \mleq{}  (r1/r(k))))


By

---

Latex:
RepeatFor  2  ((ParallelLast  THENA  ((Assert  N  \mleq{}  imax(n;N)  BY  Auto)  THEN  Auto)))

---

Home Index