---

Step * 2 1 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-k-regular(d;1;mtb-seq(mtb;mtb-point-cantor(mtb;y)))
16. ∀[X:Type]. ∀[d:metric(X)]. ∀[s:ℕ ⟶ X].  m-k-regular(d;2;s) supposing m-k-regular(d;1;s)
17. m-k-regular(d;2;mtb-seq(mtb;mtb-point-cantor(mtb;y)))
18. m-k-regular(d;2;mtb-seq(mtb;mtb-point-cantor(mtb;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 ))
BY
{ (UnfoldTopAb (-1) THEN ParallelOp -2 THEN (UnivCD THENA Auto) THEN RenameVar `j' (-2)) }

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-k-regular(d;1;mtb-seq(mtb;mtb-point-cantor(mtb;y)))
16. ∀[X:Type]. ∀[d:metric(X)]. ∀[s:ℕ ⟶ X].  m-k-regular(d;2;s) supposing m-k-regular(d;1;s)
17. ∀n,m:ℕ.
      (mdist(d;mtb-seq(mtb;mtb-point-cantor(mtb;y)) n;mtb-seq(mtb;mtb-point-cantor(mtb;y)) m) ≤ ((r(2)/r(n + 1))
      + (r(2)/r(m + 1))))
18. ∀n,m:ℕ.
      (mdist(d;mtb-seq(mtb;mtb-point-cantor(mtb;x)) n;mtb-seq(mtb;mtb-point-cantor(mtb;x)) m) ≤ ((r(2)/r(n + 1))
      + (r(2)/r(m + 1))))
19. j : ℕ
20. m : ℕ
⊢ 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 ) 
          j;mtb-seq(mtb;λi.if i <z n then mtb-point-cantor(mtb;x) i else mtb-point-cantor(mtb;y) i fi ) m) ≤ ((r(2)/r(j
+ 1))
+ (r(2)/r(m + 1)))

---

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-k-regular(d;1;mtb-seq(mtb;mtb-point-cantor(mtb;y)))
16.  \mforall{}[X:Type].  \mforall{}[d:metric(X)].  \mforall{}[s:\mBbbN{}  {}\mrightarrow{}  X].    m-k-regular(d;2;s)  supposing  m-k-regular(d;1;s)
17.  m-k-regular(d;2;mtb-seq(mtb;mtb-point-cantor(mtb;y)))
18.  m-k-regular(d;2;mtb-seq(mtb;mtb-point-cantor(mtb;x)))
\mvdash{}  m-k-regular(d;2;mtb-seq(mtb;\mlambda{}i.if  i  <z  n
                                                                  then  mtb-point-cantor(mtb;x)  i
                                                                  else  mtb-point-cantor(mtb;y)  i
                                                                  fi  ))


By

---

Latex:
(UnfoldTopAb  (-1)  THEN  ParallelOp  -2  THEN  (UnivCD  THENA  Auto)  THEN  RenameVar  `j'  (-2))

---

Home Index