---

Step * of Lemma compact-metric-to-real-continuity

No Annotations
∀[X:Type]. ∀d:metric(X). ∀c:mcompact(X;d). ∀f:FUN(X ⟶ ℝ).  UC(f:X ⟶ ℝ)
BY
{ (Auto
   THEN D 3
   THEN RenameVar `cmplt' 3
   THEN RenameVar `mtb' 4
   THEN (Assert ∀x,y:X.  (x ≡ y ⇒ ((f x) = (f y))) BY
               (D -1
                THEN (Unhide THENA Auto)
                THEN RepUR ``is-mfun`` -1
                THEN RepeatFor 3 (ParallelLast)
                THEN RWO "rmetric-meq" (-1)
                THEN Auto))
   THEN DVar `f'
   THEN Thin (-2)
   THEN RepUR ``m-unif-cont mdist rmetric`` 0
   THEN Fold `mdist` 0
   THEN Auto
   THEN (Assert ∀j:ℕ+
                  ∃n:ℕ
                   ∀p,q:mtb-cantor(mtb).
                     ((p = q ∈ (i:ℕn ⟶ ℕ(fst(mtb)) i))
                     ⇒ ((f mtb-cantor-map(d;cmplt;mtb;p) j) = (f mtb-cantor-map(d;cmplt;mtb;q) j) ∈ ℤ)) BY
               ((D 0 THENA Auto)
                THEN (InstLemma `general-cantor-to-int-uniform-continuity` [⌜fst(mtb)⌝]⋅ THENA Auto)
                THEN RepUR ``so_apply`` -1
                THEN Fold `mtb-cantor` (-1)
                THEN (D -1 With ⌜λp.(f mtb-cantor-map(d;cmplt;mtb;p) j)⌝  THENA Auto)
                THEN Reduce -1
                THEN Auto))
   THEN (D -1 With ⌜2 * k⌝  THENA Auto)
   THEN D -1) }

1
1. [X] : Type
2. d : metric(X)
3. cmplt : mcomplete(X with d)
4. mtb : m-TB(X;d)
5. f : X ⟶ ℝ
6. ∀x,y:X.  (x ≡ y ⇒ ((f x) = (f y)))
7. k : ℕ+
8. n : ℕ
9. ∀p,q:mtb-cantor(mtb).
     ((p = q ∈ (i:ℕn ⟶ ℕ(fst(mtb)) i))
     ⇒ ((f mtb-cantor-map(d;cmplt;mtb;p) (2 * k)) = (f mtb-cantor-map(d;cmplt;mtb;q) (2 * k)) ∈ ℤ))
⊢ ∃delta:{d:ℝ| r0 < d} . ∀x,y:X.  ((mdist(d;x;y) ≤ delta) ⇒ (|(f x) - f y| ≤ (r1/r(k))))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:Type].  \mforall{}d:metric(X).  \mforall{}c:mcompact(X;d).  \mforall{}f:FUN(X  {}\mrightarrow{}  \mBbbR{}).    UC(f:X  {}\mrightarrow{}  \mBbbR{})


By

---

Latex:
(Auto
  THEN  D  3
  THEN  RenameVar  `cmplt'  3
  THEN  RenameVar  `mtb'  4
  THEN  (Assert  \mforall{}x,y:X.    (x  \mequiv{}  y  {}\mRightarrow{}  ((f  x)  =  (f  y)))  BY
                          (D  -1
                            THEN  (Unhide  THENA  Auto)
                            THEN  RepUR  ``is-mfun``  -1
                            THEN  RepeatFor  3  (ParallelLast)
                            THEN  RWO  "rmetric-meq"  (-1)
                            THEN  Auto))
  THEN  DVar  `f'
  THEN  Thin  (-2)
  THEN  RepUR  ``m-unif-cont  mdist  rmetric``  0
  THEN  Fold  `mdist`  0
  THEN  Auto
  THEN  (Assert  \mforall{}j:\mBbbN{}\msupplus{}
                                \mexists{}n:\mBbbN{}
                                  \mforall{}p,q:mtb-cantor(mtb).
                                      ((p  =  q)
                                      {}\mRightarrow{}  ((f  mtb-cantor-map(d;cmplt;mtb;p)  j)
                                            =  (f  mtb-cantor-map(d;cmplt;mtb;q)  j)))  BY
                          ((D  0  THENA  Auto)
                            THEN  (InstLemma  `general-cantor-to-int-uniform-continuity`  [\mkleeneopen{}fst(mtb)\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  RepUR  ``so\_apply``  -1
                            THEN  Fold  `mtb-cantor`  (-1)
                            THEN  (D  -1  With  \mkleeneopen{}\mlambda{}p.(f  mtb-cantor-map(d;cmplt;mtb;p)  j)\mkleeneclose{}    THENA  Auto)
                            THEN  Reduce  -1
                            THEN  Auto))
  THEN  (D  -1  With  \mkleeneopen{}2  *  k\mkleeneclose{}    THENA  Auto)
  THEN  D  -1)

---

Home Index