---

Step * 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))))
⊢ x n↓ as n→∞
BY
{ ((Assert fst((x N)) ∈ T BY
          Auto)
   THEN (Assert ∀m:ℕ. ((fst((x (N + m)))) = (fst((x N))) ∈ T) BY
               ((D 0 THENA Auto)
                THEN (InstHyp [⌜N + m⌝;⌜N⌝] (-3)⋅ THENA Auto)
                THEN (RepUR ``mdist`` -1 THEN MoveToConcl (-1))
                THEN ((GenConclTerm ⌜x (N + m)⌝⋅ THENA Auto) THEN D -2)
                THEN (GenConclTerm ⌜x N⌝⋅ THENA Auto)
                THEN D -2
                THEN Reduce 0
                THEN AutoSplit
                THEN (Assert snd((X i)) ∈ (fst((X i))) ⟶ (fst((X i))) ⟶ ℝ BY
                            (GenConclTerm ⌜X i⌝⋅ THEN Auto))
                THEN Auto
                THEN nRMul ⌜r(2)⌝ (-1)⋅
                THEN RWO "rleq-int" (-1) 
                THEN Auto))
   THEN (Assert ∀m:ℕ. (snd((x (N + m))) ∈ fst((X (fst((x N)))))) BY
               (ParallelLast THEN InferEqualType THEN Auto))) }

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. [%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→∞

---

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


By

---

Latex:
((Assert  fst((x  N))  \mmember{}  T  BY
                Auto)
  THEN  (Assert  \mforall{}m:\mBbbN{}.  ((fst((x  (N  +  m))))  =  (fst((x  N))))  BY
                          ((D  0  THENA  Auto)
                            THEN  (InstHyp  [\mkleeneopen{}N  +  m\mkleeneclose{};\mkleeneopen{}N\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)
                            THEN  (RepUR  ``mdist``  -1  THEN  MoveToConcl  (-1))
                            THEN  ((GenConclTerm  \mkleeneopen{}x  (N  +  m)\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  D  -2)
                            THEN  (GenConclTerm  \mkleeneopen{}x  N\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  D  -2
                            THEN  Reduce  0
                            THEN  AutoSplit
                            THEN  (Assert  snd((X  i))  \mmember{}  (fst((X  i)))  {}\mrightarrow{}  (fst((X  i)))  {}\mrightarrow{}  \mBbbR{}  BY
                                                    (GenConclTerm  \mkleeneopen{}X  i\mkleeneclose{}\mcdot{}  THEN  Auto))
                            THEN  Auto
                            THEN  nRMul  \mkleeneopen{}r(2)\mkleeneclose{}  (-1)\mcdot{}
                            THEN  RWO  "rleq-int"  (-1) 
                            THEN  Auto))
  THEN  (Assert  \mforall{}m:\mBbbN{}.  (snd((x  (N  +  m)))  \mmember{}  fst((X  (fst((x  N))))))  BY
                          (ParallelLast  THEN  InferEqualType  THEN  Auto)))

---

Home Index