---

Step * of Lemma mtb-cantor-map-onto

∀[X:Type]. ∀[d:metric(X)]. ∀[cmplt:mcomplete(X with d)]. ∀[mtb:m-TB(X;d)]. ∀[x:X].
  mtb-cantor-map(d;cmplt;mtb;mtb-point-cantor(mtb;x)) ≡ x
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 Unfold `mtb-cantor-map` 0
   THEN (BLemma `cauchy-mlimit-unique` THEN Auto)
   THEN RWO "-2" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[d:metric(X)].  \mforall{}[cmplt:mcomplete(X  with  d)].  \mforall{}[mtb:m-TB(X;d)].  \mforall{}[x:X].
    mtb-cantor-map(d;cmplt;mtb;mtb-point-cantor(mtb;x))  \mequiv{}  x


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  Unfold  `mtb-cantor-map`  0
  THEN  (BLemma  `cauchy-mlimit-unique`  THEN  Auto)
  THEN  RWO  "-2"  0
  THEN  Auto)

---

Home Index