---

Step * of Lemma compact-metric-to-int-bounded

∀[X:Type]. ∀d:metric(X). ∀cmplt:mcomplete(X with d). ∀mtb:m-TB(X;d). ∀f:X ⟶ ℤ.  ∃B:ℕ. ∀x:X. ∃y:X. (x ≡ y ∧ (|f y| ≤ B))
BY
{ (Auto
   THEN (InstLemma `mtb-cantor-map-onto` [⌜X⌝;⌜d⌝;⌜cmplt⌝;⌜mtb⌝]⋅ THENA Auto)
   THEN (InstLemma `general-cantor-to-int-bounded` [⌜fst(mtb)⌝;⌜λp.(f mtb-cantor-map(d;cmplt;mtb;p))⌝]⋅
         THENA (Auto THEN RepeatFor 2 (DVar `mtb') THEN Reduce 0 THEN Auto)
         )
   THEN (Subst' n:ℕ ⟶ ℕfst(mtb)[n] ~ mtb-cantor(mtb) -1 THENA Computation)
   THEN ParallelLast
   THEN Reduce -1
   THEN Auto
   THEN D 0 With ⌜mtb-cantor-map(d;cmplt;mtb;mtb-point-cantor(mtb;x))⌝ 
   THEN Auto
   THEN BLemma `meq_inversion`
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}d:metric(X).  \mforall{}cmplt:mcomplete(X  with  d).  \mforall{}mtb:m-TB(X;d).  \mforall{}f:X  {}\mrightarrow{}  \mBbbZ{}.
        \mexists{}B:\mBbbN{}.  \mforall{}x:X.  \mexists{}y:X.  (x  \mequiv{}  y  \mwedge{}  (|f  y|  \mleq{}  B))


By

---

Latex:
(Auto
  THEN  (InstLemma  `mtb-cantor-map-onto`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}cmplt\mkleeneclose{};\mkleeneopen{}mtb\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `general-cantor-to-int-bounded`  [\mkleeneopen{}fst(mtb)\mkleeneclose{};\mkleeneopen{}\mlambda{}p.(f  mtb-cantor-map(d;cmplt;mtb;p))\mkleeneclose{}]
              \mcdot{}
              THENA  (Auto  THEN  RepeatFor  2  (DVar  `mtb')  THEN  Reduce  0  THEN  Auto)
              )
  THEN  (Subst'  n:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}fst(mtb)[n]  \msim{}  mtb-cantor(mtb)  -1  THENA  Computation)
  THEN  ParallelLast
  THEN  Reduce  -1
  THEN  Auto
  THEN  D  0  With  \mkleeneopen{}mtb-cantor-map(d;cmplt;mtb;mtb-point-cantor(mtb;x))\mkleeneclose{} 
  THEN  Auto
  THEN  BLemma  `meq\_inversion`
  THEN  Auto)

---

Home Index