---

Step * of Lemma mcompact_functionality

∀[X,Y:Type].  ∀d:metric(X). (mcompact(X;d) ⇐⇒ mcompact(Y;d)) supposing X ≡ Y
BY
{ ((Assert ⌜∀[X,Y:Type].  ∀d:metric(X). (mcompact(X;d) ⇒ mcompact(Y;d)) supposing X ≡ Y⌝⋅
   THENM (Auto THEN (InstHyp [⌜Y⌝;⌜X⌝;⌜d⌝] 1⋅ THEN Auto) THEN ParallelOp 4 THEN Auto)
   )
   THEN Auto
   THEN ParallelLast
   THEN All (Fold `and`)
   THEN RepeatFor 2 (ParallelLast)
   THEN All Reduce) }

1
1. [X] : Type
2. [Y] : Type
3. X ≡ Y
4. d : metric(X)
5. m-TB(X;d)
6. ∀x:ℕ ⟶ X. (mcauchy(d;n.x n) ⇒ x n↓ as n→∞)
⊢ ∀x:ℕ ⟶ Y. (mcauchy(d;n.x n) ⇒ x n↓ as n→∞)

2
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)))} 

---

Latex:

---

Latex:
\mforall{}[X,Y:Type].    \mforall{}d:metric(X).  (mcompact(X;d)  \mLeftarrow{}{}\mRightarrow{}  mcompact(Y;d))  supposing  X  \mequiv{}  Y


By

---

Latex:
((Assert  \mkleeneopen{}\mforall{}[X,Y:Type].    \mforall{}d:metric(X).  (mcompact(X;d)  {}\mRightarrow{}  mcompact(Y;d))  supposing  X  \mequiv{}  Y\mkleeneclose{}\mcdot{}
  THENM  (Auto  THEN  (InstHyp  [\mkleeneopen{}Y\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]  1\mcdot{}  THEN  Auto)  THEN  ParallelOp  4  THEN  Auto)
  )
  THEN  Auto
  THEN  ParallelLast
  THEN  All  (Fold  `and`)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  All  Reduce)

---

Home Index