---

Step * 2 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
⊢ lim n1→∞.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 )) 
           n1 = y
BY
{ (InstLemma `m-regularize-of-regular` [⌜X⌝;⌜d⌝;⌜mtb-seq(mtb;λi.if i <z n
                                                                then mtb-point-cantor(mtb;x) i
                                                                else mtb-point-cantor(mtb;y) i
                                                                fi )⌝]⋅
   THENA Auto
   ) }

1
.....antecedent..... 
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
⊢ m-k-regular(d;2;mtb-seq(mtb;λi.if i <z n then mtb-point-cantor(mtb;x) i else mtb-point-cantor(mtb;y) i fi ))

2
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)
⊢ lim n1→∞.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 )) 
           n1 = y

---

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
\mvdash{}  lim  n1\mrightarrow{}\minfty{}.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  )) 
                      n1  =  y


By

---

Latex:
(InstLemma  `m-regularize-of-regular`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}mtb-seq(mtb;\mlambda{}i.if  i  <z  n
                                                                                                                            then  mtb-point-cantor(mtb;x)  i
                                                                                                                            else  mtb-point-cantor(mtb;y)  i
                                                                                                                            fi  )\mkleeneclose{}]\mcdot{}
  THENA  Auto
  )

---

Home Index