---

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


1. k : ℕ
2. X : ℕk ⟶ MetricSpace
3. ∀i:ℕk. mcomplete(X i)
4. prod-metric(k;λi.(snd((X i)))) ∈ metric(i:ℕk ⟶ (fst((X i))))
5. x : ℕ ⟶ i:ℕk ⟶ (fst((X i)))
6. mcauchy(prod-metric(k;λi.(snd((X i))));n.x n)
7. ∀i:ℕk. mcauchy(snd((X i));n.x n i)
⊢ x n↓ as n→∞
BY
{ (Assert ∀i:ℕk. x n i↓ as n→∞ BY
         (ParallelOp 3
          THEN (D -3 With ⌜i⌝  THENA Auto)
          THEN (Subst' X i ~ <fst((X i)), snd((X i))> -2 THENA ((GenConclTerm ⌜X i⌝⋅ THENA Auto) THEN D -2 THEN Reduce 0\000C THEN Auto))
          THEN RepUR ``mcomplete`` -2
          THEN D -2 With ⌜λn.(x n i)⌝ 
          THEN Auto)) }

1
1. k : ℕ
2. X : ℕk ⟶ MetricSpace
3. ∀i:ℕk. mcomplete(X i)
4. prod-metric(k;λi.(snd((X i)))) ∈ metric(i:ℕk ⟶ (fst((X i))))
5. x : ℕ ⟶ i:ℕk ⟶ (fst((X i)))
6. mcauchy(prod-metric(k;λi.(snd((X i))));n.x n)
7. ∀i:ℕk. mcauchy(snd((X i));n.x n i)
8. ∀i:ℕk. x n i↓ as n→∞
⊢ x n↓ as n→∞

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  X  :  \mBbbN{}k  {}\mrightarrow{}  MetricSpace
3.  \mforall{}i:\mBbbN{}k.  mcomplete(X  i)
4.  prod-metric(k;\mlambda{}i.(snd((X  i))))  \mmember{}  metric(i:\mBbbN{}k  {}\mrightarrow{}  (fst((X  i))))
5.  x  :  \mBbbN{}  {}\mrightarrow{}  i:\mBbbN{}k  {}\mrightarrow{}  (fst((X  i)))
6.  mcauchy(prod-metric(k;\mlambda{}i.(snd((X  i))));n.x  n)
7.  \mforall{}i:\mBbbN{}k.  mcauchy(snd((X  i));n.x  n  i)
\mvdash{}  x  n\mdownarrow{}  as  n\mrightarrow{}\minfty{}


By

---

Latex:
(Assert  \mforall{}i:\mBbbN{}k.  x  n  i\mdownarrow{}  as  n\mrightarrow{}\minfty{}  BY
              (ParallelOp  3
                THEN  (D  -3  With  \mkleeneopen{}i\mkleeneclose{}    THENA  Auto)
                THEN  (Subst'  X  i  \msim{}  <fst((X  i)),  snd((X  i))>  -2
                            THENA  ((GenConclTerm  \mkleeneopen{}X  i\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  D  -2  THEN  Reduce  0  THEN  Auto)
                            )
                THEN  RepUR  ``mcomplete``  -2
                THEN  D  -2  With  \mkleeneopen{}\mlambda{}n.(x  n  i)\mkleeneclose{} 
                THEN  Auto))

---

Home Index