Step
*
1
1
2
2
1
1
2
2
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. ∀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))))
13. ∀x@0:ℕ ⟶ (fst((X (fst((x N)))))). (mcauchy(snd((X (fst((x N)))));n.x@0 n) ⇒ x@0 n↓ as n→∞)
14. y : fst((X (fst((x N)))))
15. ∀k:ℕ+. (∃N@0:ℕ [(∀n:ℕ. ((N@0 ≤ n) ⇒ (mdist(snd((X (fst((x N)))));snd((x (N + n)));y) ≤ (r1/r(k)))))])
16. k : ℕ+
17. M : ℕ
18. ∀n:ℕ. ((M ≤ n) ⇒ (mdist(snd((X (fst((x N)))));snd((x (N + n)));y) ≤ (r1/r(k))))
⊢ ∀n:ℕ
(((N + M) ≤ n)
⇒ (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;<fst((x \000CN))
, y
>) ≤ (r1/r(k\000C))))
BY
{ RepeatFor 2 ((D 0 THENA 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. ∀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))))
13. ∀x@0:ℕ ⟶ (fst((X (fst((x N)))))). (mcauchy(snd((X (fst((x N)))));n.x@0 n) ⇒ x@0 n↓ as n→∞)
14. y : fst((X (fst((x N)))))
15. ∀k:ℕ+. (∃N@0:ℕ [(∀n:ℕ. ((N@0 ≤ n) ⇒ (mdist(snd((X (fst((x N)))));snd((x (N + n)));y) ≤ (r1/r(k)))))])
16. k : ℕ+
17. M : ℕ
18. ∀n:ℕ. ((M ≤ n) ⇒ (mdist(snd((X (fst((x N)))));snd((x (N + n)));y) ≤ (r1/r(k))))
19. n : ℕ
20. (N + M) ≤ n
⊢ 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;<fst((x N)), y\000C>) ≤ (r1/r(k))
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. \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))))))
12. mcauchy(snd((X (fst((x N)))));m.snd((x (N + m))))
13. \mforall{}x@0:\mBbbN{} {}\mrightarrow{} (fst((X (fst((x N)))))). (mcauchy(snd((X (fst((x N)))));n.x@0 n) {}\mRightarrow{} x@0 n\mdownarrow{} as n\mrightarrow{}\minfty{})
14. y : fst((X (fst((x N)))))
15. \mforall{}k:\mBbbN{}\msupplus{}
(\mexists{}N@0:\mBbbN{} [(\mforall{}n:\mBbbN{}
((N@0 \mleq{} n) {}\mRightarrow{} (mdist(snd((X (fst((x N)))));snd((x (N + n)));y) \mleq{} (r1/r(k)))))])
16. k : \mBbbN{}\msupplus{}
17. M : \mBbbN{}
18. \mforall{}n:\mBbbN{}. ((M \mleq{} n) {}\mRightarrow{} (mdist(snd((X (fst((x N)))));snd((x (N + n)));y) \mleq{} (r1/r(k))))
\mvdash{} \mforall{}n:\mBbbN{}
(((N + M) \mleq{} n)
{}\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;<fst((x N)),\000C y>) \mleq{} (r1/r(k))))
By
Latex:
RepeatFor 2 ((D 0 THENA Auto))
Home
Index