---

Step * 1 1 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))))))
⊢ x n↓ as n→∞
BY
{ (Assert mcauchy(snd((X (fst((x N)))));m.snd((x (N + m)))) BY
         (ParallelOp 6
          THEN (D 0 THENA Auto)
          THEN (D 6 With ⌜k + 1⌝  THENA Auto)
          THEN ExRepD
          THEN RepUR ``mdist`` -1
          THEN RepUR ``mdist`` 0
          THEN (D 0 With ⌜imax(0;N1 - N)⌝ 
                THENA (Auto
                       THEN (Assert snd((X (fst((x N))))) ∈ (fst((X (fst((x N)))))) ⟶ (fst((X (fst((x N)))))) ⟶ ℝ BY
                                   (GenConclTerm ⌜X (fst((x N)))⌝⋅ THEN Auto))
                       THEN Auto)
                )
          THEN Auto
          THEN (InstHyp [⌜N + m⌝;⌜N + m@0⌝] (-5)⋅
                THENA (Auto THEN (RWO "-2< -1<" 0 THENA Auto) THEN (RWO "imax_unfold" 0 THENA Auto) THEN AutoSplit)
                )
          THEN MoveToConcl (-1)
          THEN GenConclTerms Auto [⌜x (N + m)⌝;⌜x (N + m@0)⌝]⋅
          THEN D -4
          THEN D -2
          THEN Reduce 0)) }

1
.....aux..... 
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. N : ℕ
7. ∀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))))
8. fst((x N)) ∈ T
9. ∀m:ℕ. ((fst((x (N + m)))) = (fst((x N))) ∈ T)
10. ∀m:ℕ. (snd((x (N + m))) ∈ fst((X (fst((x N))))))
11. k : ℕ+
12. N1 : ℕ
13. ∀n,m:ℕ.
      ((N1 ≤ n)
      ⇒ (N1 ≤ m)
      ⇒ (let i,v = x n 
          in let j,w = x m 
             in if eq i j then rmin((snd((X i))) v w;r1) else r1 fi  ≤ (r1/r(k + 1))))
14. m : ℕ
15. m@0 : ℕ
16. imax(0;N1 - N) ≤ m
17. imax(0;N1 - N) ≤ m@0
18. i : T
19. v2 : fst((X i))
20. (x (N + m)) = <i, v2> ∈ (i:T × (fst((X i))))
21. i1 : T
22. v3 : fst((X i1))
23. (x (N + m@0)) = <i1, v3> ∈ (i:T × (fst((X i))))
⊢ (if eq i i1 then rmin((snd((X i))) v2 v3;r1) else r1 fi  ≤ (r1/r(k + 1)))
⇒ (((snd((X (fst((x N)))))) v2 v3) ≤ (r1/r(k)))

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. [%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))))
⊢ x n↓ as n→∞

---

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))))))
\mvdash{}  x  n\mdownarrow{}  as  n\mrightarrow{}\minfty{}


By

---

Latex:
(Assert  mcauchy(snd((X  (fst((x  N)))));m.snd((x  (N  +  m))))  BY
              (ParallelOp  6
                THEN  (D  0  THENA  Auto)
                THEN  (D  6  With  \mkleeneopen{}k  +  1\mkleeneclose{}    THENA  Auto)
                THEN  ExRepD
                THEN  RepUR  ``mdist``  -1
                THEN  RepUR  ``mdist``  0
                THEN  (D  0  With  \mkleeneopen{}imax(0;N1  -  N)\mkleeneclose{} 
                            THENA  (Auto
                                          THEN  (Assert  snd((X  (fst((x  N)))))  \mmember{}  (fst((X  (fst((x  N))))))
                                                                    {}\mrightarrow{}  (fst((X  (fst((x  N))))))
                                                                    {}\mrightarrow{}  \mBbbR{}  BY
                                                                  (GenConclTerm  \mkleeneopen{}X  (fst((x  N)))\mkleeneclose{}\mcdot{}  THEN  Auto))
                                          THEN  Auto)
                            )
                THEN  Auto
                THEN  (InstHyp  [\mkleeneopen{}N  +  m\mkleeneclose{};\mkleeneopen{}N  +  m@0\mkleeneclose{}]  (-5)\mcdot{}
                            THENA  (Auto
                                          THEN  (RWO  "-2<  -1<"  0  THENA  Auto)
                                          THEN  (RWO  "imax\_unfold"  0  THENA  Auto)
                                          THEN  AutoSplit)
                            )
                THEN  MoveToConcl  (-1)
                THEN  GenConclTerms  Auto  [\mkleeneopen{}x  (N  +  m)\mkleeneclose{};\mkleeneopen{}x  (N  +  m@0)\mkleeneclose{}]\mcdot{}
                THEN  D  -4
                THEN  D  -2
                THEN  Reduce  0))

---

Home Index