---

Step * 2 of Lemma mcompact_functionality


1. [X] : Type
2. [Y] : Type
3. X ≡ Y
4. d : metric(X)
5. mcomplete(X with d)
6. {tb:B:ℕ ⟶ ℕ+ × k:ℕ ⟶ ℕB k ⟶ X × (X ⟶ k:ℕ ⟶ ℕB k)| 
    let B,xs,c = tb in 
    ∀p:X. ∀k:ℕ.  (mdist(d;p;xs k (c p k)) ≤ (r1/r(k + 1)))} 
⊢ {tb:B:ℕ ⟶ ℕ+ × k:ℕ ⟶ ℕB k ⟶ Y × (Y ⟶ k:ℕ ⟶ ℕB k)| 
   let B,xs,c = tb in 
   ∀p:Y. ∀k:ℕ.  (mdist(d;p;xs k (c p k)) ≤ (r1/r(k + 1)))} 
BY
{ D -1 }

1
1. [X] : Type
2. [Y] : Type
3. X ≡ Y
4. d : metric(X)
5. mcomplete(X with d)
6. tb : B:ℕ ⟶ ℕ+ × k:ℕ ⟶ ℕB k ⟶ X × (X ⟶ k:ℕ ⟶ ℕB k)
7. [%5] : let B,xs,c = tb in 
∀p:X. ∀k:ℕ.  (mdist(d;p;xs k (c p k)) ≤ (r1/r(k + 1)))
⊢ {tb:B:ℕ ⟶ ℕ+ × k:ℕ ⟶ ℕB k ⟶ Y × (Y ⟶ k:ℕ ⟶ ℕB k)| 
   let B,xs,c = tb in 
   ∀p:Y. ∀k:ℕ.  (mdist(d;p;xs k (c p k)) ≤ (r1/r(k + 1)))} 

---

Latex:

---

Latex:

1.  [X]  :  Type
2.  [Y]  :  Type
3.  X  \mequiv{}  Y
4.  d  :  metric(X)
5.  mcomplete(X  with  d)
6.  \{tb:B:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}  \mtimes{}  k:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B  k  {}\mrightarrow{}  X  \mtimes{}  (X  {}\mrightarrow{}  k:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B  k)| 
        let  B,xs,c  =  tb  in 
        \mforall{}p:X.  \mforall{}k:\mBbbN{}.    (mdist(d;p;xs  k  (c  p  k))  \mleq{}  (r1/r(k  +  1)))\} 
\mvdash{}  \{tb:B:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}  \mtimes{}  k:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B  k  {}\mrightarrow{}  Y  \mtimes{}  (Y  {}\mrightarrow{}  k:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B  k)| 
      let  B,xs,c  =  tb  in 
      \mforall{}p:Y.  \mforall{}k:\mBbbN{}.    (mdist(d;p;xs  k  (c  p  k))  \mleq{}  (r1/r(k  +  1)))\} 


By

---

Latex:
D  -1

---

Home Index