---

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

∀[X:Type]
  ∀d:metric(X). ∀cmplt:mcomplete(X with d). ∀mtb:m-TB(X;d). ∀n:ℕ. ∀x,y:X.
    ((mdist(d;x;y) ≤ (r1/r(n + 1)))
    ⇒ (∃p,q:mtb-cantor(mtb)
         ((p = q ∈ (i:ℕn ⟶ ℕ(fst(mtb)) i)) ∧ mtb-cantor-map(d;cmplt;mtb;p) ≡ x ∧ mtb-cantor-map(d;cmplt;mtb;q) ≡ y)))
BY
{ (Auto
   THEN (InstLemma `mtb-point-cantor-seq-regular` [⌜X⌝;⌜d⌝;⌜mtb⌝;⌜x⌝]⋅ THENA Auto)
   THEN (InstLemma `m-regularize-of-regular` [⌜X⌝;⌜d⌝;⌜mtb-seq(mtb;mtb-point-cantor(mtb;x))⌝]⋅
         THENA (Auto THEN InstLemma `m-k-regular-monotone` [⌜1⌝;⌜2⌝]⋅ THEN Auto)
         )
   THEN (InstLemma `m-regularize-mcauchy` [⌜X⌝;⌜d⌝]⋅ THENA Auto)
   THEN (Assert mtb-cantor(mtb) ⊆r (i:ℕn ⟶ ℕ(fst(mtb)) i) BY
               (Unfold `mtb-cantor` 0 THEN RepeatFor 2 (DVar `mtb') THEN Auto))
   THEN (D 0 With ⌜mtb-point-cantor(mtb;x)⌝  THENA (Auto THEN RepeatFor 2 (DVar `mtb') THEN Auto))
   THEN (D 0 With ⌜λi.if i <z n then mtb-point-cantor(mtb;x) i else mtb-point-cantor(mtb;y) i fi ⌝ 
         THENA (Auto THEN RepeatFor 2 (DVar `mtb') THEN 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)
⊢ mtb-cantor-map(d;cmplt;mtb;mtb-point-cantor(mtb;x)) ≡ x

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
⊢ mtb-cantor-map(d;cmplt;mtb;λi.if i <z n then mtb-point-cantor(mtb;x) i else mtb-point-cantor(mtb;y) i fi ) ≡ y

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}d:metric(X).  \mforall{}cmplt:mcomplete(X  with  d).  \mforall{}mtb:m-TB(X;d).  \mforall{}n:\mBbbN{}.  \mforall{}x,y:X.
        ((mdist(d;x;y)  \mleq{}  (r1/r(n  +  1)))
        {}\mRightarrow{}  (\mexists{}p,q:mtb-cantor(mtb)
                  ((p  =  q)  \mwedge{}  mtb-cantor-map(d;cmplt;mtb;p)  \mequiv{}  x  \mwedge{}  mtb-cantor-map(d;cmplt;mtb;q)  \mequiv{}  y)))


By

---

Latex:
(Auto
  THEN  (InstLemma  `mtb-point-cantor-seq-regular`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}mtb\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `m-regularize-of-regular`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}mtb-seq(mtb;mtb-point-cantor(mtb;x))\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  InstLemma  `m-k-regular-monotone`  [\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THEN  Auto)
              )
  THEN  (InstLemma  `m-regularize-mcauchy`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  mtb-cantor(mtb)  \msubseteq{}r  (i:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}(fst(mtb))  i)  BY
                          (Unfold  `mtb-cantor`  0  THEN  RepeatFor  2  (DVar  `mtb')  THEN  Auto))
  THEN  (D  0  With  \mkleeneopen{}mtb-point-cantor(mtb;x)\mkleeneclose{}    THENA  (Auto  THEN  RepeatFor  2  (DVar  `mtb')  THEN  Auto))
  THEN  (D  0  With  \mkleeneopen{}\mlambda{}i.if  i  <z  n  then  mtb-point-cantor(mtb;x)  i  else  mtb-point-cantor(mtb;y)  i  fi  \mkleeneclose{} 
              THENA  (Auto  THEN  RepeatFor  2  (DVar  `mtb')  THEN  Auto)
              )
  THEN  Auto)

---

Home Index