---

Step * of Lemma union-metric-space-complete

∀T:Type. ∀eq:EqDecider(T). ∀X:T ⟶ MetricSpace.  ((∀i:T. mcomplete(X i)) ⇒ mcomplete(union-metric-space(T;eq;X)))
BY
{ (Auto
   THEN RepUR ``union-metric-space mcomplete`` 0
   THEN Auto
   THEN (DupHyp (-1) THEN (D -1 With ⌜2⌝  THENA Auto))
   THEN ExRepD) }

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

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}eq:EqDecider(T).  \mforall{}X:T  {}\mrightarrow{}  MetricSpace.
    ((\mforall{}i:T.  mcomplete(X  i))  {}\mRightarrow{}  mcomplete(union-metric-space(T;eq;X)))


By

---

Latex:
(Auto
  THEN  RepUR  ``union-metric-space  mcomplete``  0
  THEN  Auto
  THEN  (DupHyp  (-1)  THEN  (D  -1  With  \mkleeneopen{}2\mkleeneclose{}    THENA  Auto))
  THEN  ExRepD)

---

Home Index