---

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


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)) ∈ ℤ))
10. delta : {d:ℝ| r0 < d} 
11. ∀x,y:X.
      ((mdist(d;x;y) ≤ delta)
      ⇒ (∃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)))
12. x : X
13. ∀y:X
      ((mdist(d;x;y) ≤ delta)
      ⇒ (∃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)))
14. y : X
15. mdist(d;x;y) ≤ delta
16. p : mtb-cantor(mtb)
17. q : mtb-cantor(mtb)
18. p = q ∈ (i:ℕn ⟶ ℕ(fst(mtb)) i)
19. mtb-cantor-map(d;cmplt;mtb;p) ≡ x
20. mtb-cantor-map(d;cmplt;mtb;q) ≡ y
⊢ |(f x) - f y| ≤ (r1/r(k))
BY
{ (FHyp 9 [-3] THENA Auto) }

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)) ∈ ℤ))
10. delta : {d:ℝ| r0 < d} 
11. ∀x,y:X.
      ((mdist(d;x;y) ≤ delta)
      ⇒ (∃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)))
12. x : X
13. ∀y:X
      ((mdist(d;x;y) ≤ delta)
      ⇒ (∃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)))
14. y : X
15. mdist(d;x;y) ≤ delta
16. p : mtb-cantor(mtb)
17. q : mtb-cantor(mtb)
18. p = q ∈ (i:ℕn ⟶ ℕ(fst(mtb)) i)
19. mtb-cantor-map(d;cmplt;mtb;p) ≡ x
20. mtb-cantor-map(d;cmplt;mtb;q) ≡ y
21. (f mtb-cantor-map(d;cmplt;mtb;p) (2 * k)) = (f mtb-cantor-map(d;cmplt;mtb;q) (2 * k)) ∈ ℤ
⊢ |(f x) - f y| ≤ (r1/r(k))

---

Latex:

---

Latex:

1.  [X]  :  Type
2.  d  :  metric(X)
3.  cmplt  :  mcomplete(X  with  d)
4.  mtb  :  m-TB(X;d)
5.  f  :  X  {}\mrightarrow{}  \mBbbR{}
6.  \mforall{}x,y:X.    (x  \mequiv{}  y  {}\mRightarrow{}  ((f  x)  =  (f  y)))
7.  k  :  \mBbbN{}\msupplus{}
8.  n  :  \mBbbN{}
9.  \mforall{}p,q:mtb-cantor(mtb).
          ((p  =  q)
          {}\mRightarrow{}  ((f  mtb-cantor-map(d;cmplt;mtb;p)  (2  *  k))  =  (f  mtb-cantor-map(d;cmplt;mtb;q)  (2  *  k))))
10.  delta  :  \{d:\mBbbR{}|  r0  <  d\} 
11.  \mforall{}x,y:X.
            ((mdist(d;x;y)  \mleq{}  delta)
            {}\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)))
12.  x  :  X
13.  \mforall{}y:X
            ((mdist(d;x;y)  \mleq{}  delta)
            {}\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)))
14.  y  :  X
15.  mdist(d;x;y)  \mleq{}  delta
16.  p  :  mtb-cantor(mtb)
17.  q  :  mtb-cantor(mtb)
18.  p  =  q
19.  mtb-cantor-map(d;cmplt;mtb;p)  \mequiv{}  x
20.  mtb-cantor-map(d;cmplt;mtb;q)  \mequiv{}  y
\mvdash{}  |(f  x)  -  f  y|  \mleq{}  (r1/r(k))


By

---

Latex:
(FHyp  9  [-3]  THENA  Auto)

---

Home Index