---

Step * 2 1 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)
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)))} 
BY
{ ((UseWitness ⌜tb⌝⋅ THEN MemTypeCD) THEN Auto THEN RepeatFor 2 (D -2) THEN All Reduce THEN ParallelLast) }

---

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)
7.  [\%5]  :  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:
((UseWitness  \mkleeneopen{}tb\mkleeneclose{}\mcdot{}  THEN  MemTypeCD)
  THEN  Auto
  THEN  RepeatFor  2  (D  -2)
  THEN  All  Reduce
  THEN  ParallelLast)

---

Home Index