---

Step * 1 1 2 2 1 1 3 of Lemma union-metric-space-complete

.....wf..... 
1. T : Type
2. eq : EqDecider(T)
3. X : T ⟶ MetricSpace
4. ∀i:T. mcomplete(X i)
5. x : ℕ ⟶ (i:T × (fst((X i))))
6. mcauchy(λp,q. let i,v = p in let j,w = q in if eq i j then rmin(mdist(snd((X i));v;w);r1) else r1 fi ;n.x n)
7. N : ℕ
8. ∀n,m:ℕ.
     ((N ≤ n)
     ⇒ (N ≤ m)
     ⇒ (mdist(λp,q. let i,v = p 
                     in let j,w = q 
                        in if eq i j then rmin(mdist(snd((X i));v;w);r1) else r1 fi ;x n;x m) ≤ (r1/r(2))))
9. fst((x N)) ∈ T
10. ∀m:ℕ. ((fst((x (N + m)))) = (fst((x N))) ∈ T)
11. ∀m:ℕ. (snd((x (N + m))) ∈ fst((X (fst((x N))))))
12. mcauchy(snd((X (fst((x N)))));m.snd((x (N + m))))
13. ∀x@0:ℕ ⟶ (fst((X (fst((x N)))))). (mcauchy(snd((X (fst((x N)))));n.x@0 n) ⇒ x@0 n↓ as n→∞)
14. y : fst((X (fst((x N)))))
15. lim n→∞.snd((x (N + n))) = y
16. y1 : i:T × (fst((X i)))
⊢ istype(lim n→∞.x n = y1)
BY
{ At ⌜Type⌝ (D 0)⋅ }

1
1. T : Type
2. eq : EqDecider(T)
3. X : T ⟶ MetricSpace
4. ∀i:T. mcomplete(X i)
5. x : ℕ ⟶ (i:T × (fst((X i))))
6. mcauchy(λp,q. let i,v = p in let j,w = q in if eq i j then rmin(mdist(snd((X i));v;w);r1) else r1 fi ;n.x n)
7. N : ℕ
8. ∀n,m:ℕ.
     ((N ≤ n)
     ⇒ (N ≤ m)
     ⇒ (mdist(λp,q. let i,v = p 
                     in let j,w = q 
                        in if eq i j then rmin(mdist(snd((X i));v;w);r1) else r1 fi ;x n;x m) ≤ (r1/r(2))))
9. fst((x N)) ∈ T
10. ∀m:ℕ. ((fst((x (N + m)))) = (fst((x N))) ∈ T)
11. ∀m:ℕ. (snd((x (N + m))) ∈ fst((X (fst((x N))))))
12. mcauchy(snd((X (fst((x N)))));m.snd((x (N + m))))
13. ∀x@0:ℕ ⟶ (fst((X (fst((x N)))))). (mcauchy(snd((X (fst((x N)))));n.x@0 n) ⇒ x@0 n↓ as n→∞)
14. y : fst((X (fst((x N)))))
15. lim n→∞.snd((x (N + n))) = y
16. y1 : i:T × (fst((X i)))
⊢ lim n→∞.x n = y1 ∈ Type

---

Latex:

---

Latex:
.....wf..... 
1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  X  :  T  {}\mrightarrow{}  MetricSpace
4.  \mforall{}i:T.  mcomplete(X  i)
5.  x  :  \mBbbN{}  {}\mrightarrow{}  (i:T  \mtimes{}  (fst((X  i))))
6.  mcauchy(\mlambda{}p,q.  let  i,v  =  p 
                                  in  let  j,w  =  q 
                                        in  if  eq  i  j  then  rmin(mdist(snd((X  i));v;w);r1)  else  r1  fi  ;n.x  n)
7.  N  :  \mBbbN{}
8.  \mforall{}n,m:\mBbbN{}.
          ((N  \mleq{}  n)
          {}\mRightarrow{}  (N  \mleq{}  m)
          {}\mRightarrow{}  (mdist(\mlambda{}p,q.  let  i,v  =  p 
                                          in  let  j,w  =  q 
                                                in  if  eq  i  j  then  rmin(mdist(snd((X  i));v;w);r1)  else  r1  fi  ;x 
                                                                                                                                                                  n;x 
                                                                                                                                                                      m)  \mleq{}  (r1/r(2))))
9.  fst((x  N))  \mmember{}  T
10.  \mforall{}m:\mBbbN{}.  ((fst((x  (N  +  m))))  =  (fst((x  N))))
11.  \mforall{}m:\mBbbN{}.  (snd((x  (N  +  m)))  \mmember{}  fst((X  (fst((x  N))))))
12.  mcauchy(snd((X  (fst((x  N)))));m.snd((x  (N  +  m))))
13.  \mforall{}x@0:\mBbbN{}  {}\mrightarrow{}  (fst((X  (fst((x  N)))))).  (mcauchy(snd((X  (fst((x  N)))));n.x@0  n)  {}\mRightarrow{}  x@0  n\mdownarrow{}  as  n\mrightarrow{}\minfty{})
14.  y  :  fst((X  (fst((x  N)))))
15.  lim  n\mrightarrow{}\minfty{}.snd((x  (N  +  n)))  =  y
16.  y1  :  i:T  \mtimes{}  (fst((X  i)))
\mvdash{}  istype(lim  n\mrightarrow{}\minfty{}.x  n  =  y1)


By

---

Latex:
At  \mkleeneopen{}Type\mkleeneclose{}  (D  0)\mcdot{}

---

Home Index