---

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

.....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)))
BY
{ ((Assert (fst((x (N + m)))) = (fst((x N))) ∈ T BY
          Auto)
   THEN (Assert (fst((x (N + m@0)))) = (fst((x N))) ∈ T BY
               Auto)
   THEN (Assert (fst((x N))) = i ∈ T BY
               Auto)
   THEN (Assert (fst((x N))) = i1 ∈ T BY
               Auto)
   THEN AutoSplit
   THEN Fold `mdist` 0
   THEN (Assert (snd((X i))) = (snd((X (fst((x N)))))) ∈ metric(fst((X (fst((x N)))))) BY
               (RWO "-2" 0 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. 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))))
24. (fst((x (N + m)))) = (fst((x N))) ∈ T
25. (fst((x (N + m@0)))) = (fst((x N))) ∈ T
26. (fst((x N))) = i ∈ T
27. (fst((x N))) = i1 ∈ T
28. i = i1 ∈ T
29. (snd((X i))) = (snd((X (fst((x N)))))) ∈ metric(fst((X (fst((x N))))))
⊢ (rmin(mdist(snd((X i));v2;v3);r1) ≤ (r1/r(k + 1))) ⇒ (mdist(snd((X (fst((x N)))));v2;v3) ≤ (r1/r(k)))

---

Latex:

---

Latex:
.....aux..... 
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.  N  :  \mBbbN{}
7.  \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))))
8.  fst((x  N))  \mmember{}  T
9.  \mforall{}m:\mBbbN{}.  ((fst((x  (N  +  m))))  =  (fst((x  N))))
10.  \mforall{}m:\mBbbN{}.  (snd((x  (N  +  m)))  \mmember{}  fst((X  (fst((x  N))))))
11.  k  :  \mBbbN{}\msupplus{}
12.  N1  :  \mBbbN{}
13.  \mforall{}n,m:\mBbbN{}.
            ((N1  \mleq{}  n)
            {}\mRightarrow{}  (N1  \mleq{}  m)
            {}\mRightarrow{}  (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    \mleq{}  (r1/r(k  +  1))))
14.  m  :  \mBbbN{}
15.  m@0  :  \mBbbN{}
16.  imax(0;N1  -  N)  \mleq{}  m
17.  imax(0;N1  -  N)  \mleq{}  m@0
18.  i  :  T
19.  v2  :  fst((X  i))
20.  (x  (N  +  m))  =  <i,  v2>
21.  i1  :  T
22.  v3  :  fst((X  i1))
23.  (x  (N  +  m@0))  =  <i1,  v3>
\mvdash{}  (if  eq  i  i1  then  rmin((snd((X  i)))  v2  v3;r1)  else  r1  fi    \mleq{}  (r1/r(k  +  1)))
{}\mRightarrow{}  (((snd((X  (fst((x  N))))))  v2  v3)  \mleq{}  (r1/r(k)))


By

---

Latex:
((Assert  (fst((x  (N  +  m))))  =  (fst((x  N)))  BY
                Auto)
  THEN  (Assert  (fst((x  (N  +  m@0))))  =  (fst((x  N)))  BY
                          Auto)
  THEN  (Assert  (fst((x  N)))  =  i  BY
                          Auto)
  THEN  (Assert  (fst((x  N)))  =  i1  BY
                          Auto)
  THEN  AutoSplit
  THEN  Fold  `mdist`  0
  THEN  (Assert  (snd((X  i)))  =  (snd((X  (fst((x  N))))))  BY
                          (RWO  "-2"  0  THEN  Auto)))

---

Home Index