---

Step * 2 1 2 1 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))))
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))
BY
{ (NthHypSq (-1) THEN RepeatFor 2 ((EqCD THEN Try (Trivial)))) }

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))
⊢ mtb-seq(mtb;λi.if i <z n then mtb-point-cantor(mtb;x) i else mtb-point-cantor(mtb;y) i fi ) n1 
~ mtb-seq(mtb;mtb-point-cantor(mtb;y)) n1

---

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))))
20.  n1  :  \mBbbN{}
21.  imax(n;N)  \mleq{}  n1
22.  mdist(d;mtb-seq(mtb;mtb-point-cantor(mtb;y))  n1;y)  \mleq{}  (r1/r(k))
\mvdash{}  mdist(d;mtb-seq(mtb;...) 
                    n1;y)  \mleq{}  (r1/r(k))


By

---

Latex:
(NthHypSq  (-1)  THEN  RepeatFor  2  ((EqCD  THEN  Try  (Trivial))))

---

Home Index