Proof of Nuprl Lemma : union-metric-space-complete

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

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. [%5] : ∀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
⊢ lim n→∞.x n = <fst((x N)), y>
BY
{ (RepeatFor 2 (ParallelLast) THEN D -1 THEN RenameVar `M' (-2) THEN D 0 With ⌜N + M⌝ ) }

1
.....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. ∀k:ℕ⁺. (∃N@0:ℕ [(∀n:ℕ. ((N@0 ≤ n) ⇒ (mdist(snd((X (fst((x N)))));snd((x (N + n)));y) ≤ (r1/r(k)))))])
16. k : ℕ⁺
17. M : ℕ
18. ∀n:ℕ. ((M ≤ n) ⇒ (mdist(snd((X (fst((x N)))));snd((x (N + n)));y) ≤ (r1/r(k))))
⊢ N + M ∈ ℕ

2
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. ∀k:ℕ⁺. (∃N@0:ℕ [(∀n:ℕ. ((N@0 ≤ n) ⇒ (mdist(snd((X (fst((x N)))));snd((x (N + n)));y) ≤ (r1/r(k)))))])
16. k : ℕ⁺
17. M : ℕ
18. ∀n:ℕ. ((M ≤ n) ⇒ (mdist(snd((X (fst((x N)))));snd((x (N + n)));y) ≤ (r1/r(k))))
⊢ ∀n:ℕ
(((N + M) ≤ n)
⇒

 (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;<fst((x \000CN))

                                                                                                            , y

                                                                                                            >) ≤ (r1/r(k\000C))))

3
.....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. ∀k:ℕ⁺. (∃N@0:ℕ [(∀n:ℕ. ((N@0 ≤ n) ⇒ (mdist(snd((X (fst((x N)))));snd((x (N + n)));y) ≤ (r1/r(k)))))])
16. k : ℕ⁺
17. M : ℕ
18. ∀n:ℕ. ((M ≤ n) ⇒ (mdist(snd((X (fst((x N)))));snd((x (N + n)));y) ≤ (r1/r(k))))
19. N@0 : ℕ
⊢ istype(∀n:ℕ
           ((N@0 ≤ n)
           ⇒ (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;<fst((x N)), y>) ≤ (r1/r(\000Ck)))))

Latex:

Latex:
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. [\%5] : \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 \mvdash{} lim n\mrightarrow{}\minfty{}.x n = <fst((x N)), y> By Latex: (RepeatFor 2 (ParallelLast) THEN D -1 THEN RenameVar `M' (-2) THEN D 0 With \mkleeneopen{}N + M\mkleeneclose{} ) Home Index