Step
*
2
1
1
1
1
1
of Lemma
mtb-cantor-map-onto-common
1. X : Type
2. d : metric(X)
3. cmplt : mcomplete(X with d)
4. mtb : m-TB(X;d)
5. n : ℕ
6. x : X
7. y : X
8. mdist(d;x;y) ≤ (r1/r(n + 1))
9. m-k-regular(d;1;mtb-seq(mtb;mtb-point-cantor(mtb;x)))
10. m-regularize(d;mtb-seq(mtb;mtb-point-cantor(mtb;x))) = mtb-seq(mtb;mtb-point-cantor(mtb;x)) ∈ (ℕ ⟶ X)
11. ∀[s:ℕ ⟶ X]. (λk.(6 * k) ∈ mcauchy(d;n.m-regularize(d;s) n))
12. mtb-cantor(mtb) ⊆r (i:ℕn ⟶ ℕ(fst(mtb)) i)
13. mtb-point-cantor(mtb;x)
= (λi.if i <z n then mtb-point-cantor(mtb;x) i else mtb-point-cantor(mtb;y) i fi )
∈ (i:ℕn ⟶ ℕ(fst(mtb)) i)
14. mtb-cantor-map(d;cmplt;mtb;mtb-point-cantor(mtb;x)) ≡ x
15. m-k-regular(d;1;mtb-seq(mtb;mtb-point-cantor(mtb;y)))
16. ∀[X:Type]. ∀[d:metric(X)]. ∀[s:ℕ ⟶ X]. m-k-regular(d;2;s) supposing m-k-regular(d;1;s)
17. ∀n,m:ℕ.
(mdist(d;mtb-seq(mtb;mtb-point-cantor(mtb;y)) n;mtb-seq(mtb;mtb-point-cantor(mtb;y)) m) ≤ ((r(2)/r(n + 1))
+ (r(2)/r(m + 1))))
18. ∀n,m:ℕ.
(mdist(d;mtb-seq(mtb;mtb-point-cantor(mtb;x)) n;mtb-seq(mtb;mtb-point-cantor(mtb;x)) m) ≤ ((r(2)/r(n + 1))
+ (r(2)/r(m + 1))))
19. j : ℕ
20. m : ℕ
⊢ mdist(d;mtb-seq(mtb;λi.if i <z n then mtb-point-cantor(mtb;x) i else mtb-point-cantor(mtb;y) i fi )
j;mtb-seq(mtb;λi.if i <z n then mtb-point-cantor(mtb;x) i else mtb-point-cantor(mtb;y) i fi ) m) ≤ ((r(2)/r(j
+ 1))
+ (r(2)/r(m + 1)))
BY
{ Assert ⌜∀x,y:X.
((mdist(d;x;y) ≤ (r1/r(n + 1)))
⇒ (∀j:ℕn. ∀m:{n...}.
(mdist(d;mtb-seq(mtb;mtb-point-cantor(mtb;x)) j;mtb-seq(mtb;mtb-point-cantor(mtb;y)) m) ≤ ((r(2)/r(j
+ 1))
+ (r(2)/r(m + 1))))))⌝⋅ }
1
.....assertion.....
1. X : Type
2. d : metric(X)
3. cmplt : mcomplete(X with d)
4. mtb : m-TB(X;d)
5. n : ℕ
6. x : X
7. y : X
8. mdist(d;x;y) ≤ (r1/r(n + 1))
9. m-k-regular(d;1;mtb-seq(mtb;mtb-point-cantor(mtb;x)))
10. m-regularize(d;mtb-seq(mtb;mtb-point-cantor(mtb;x))) = mtb-seq(mtb;mtb-point-cantor(mtb;x)) ∈ (ℕ ⟶ X)
11. ∀[s:ℕ ⟶ X]. (λk.(6 * k) ∈ mcauchy(d;n.m-regularize(d;s) n))
12. mtb-cantor(mtb) ⊆r (i:ℕn ⟶ ℕ(fst(mtb)) i)
13. mtb-point-cantor(mtb;x)
= (λi.if i <z n then mtb-point-cantor(mtb;x) i else mtb-point-cantor(mtb;y) i fi )
∈ (i:ℕn ⟶ ℕ(fst(mtb)) i)
14. mtb-cantor-map(d;cmplt;mtb;mtb-point-cantor(mtb;x)) ≡ x
15. m-k-regular(d;1;mtb-seq(mtb;mtb-point-cantor(mtb;y)))
16. ∀[X:Type]. ∀[d:metric(X)]. ∀[s:ℕ ⟶ X]. m-k-regular(d;2;s) supposing m-k-regular(d;1;s)
17. ∀n,m:ℕ.
(mdist(d;mtb-seq(mtb;mtb-point-cantor(mtb;y)) n;mtb-seq(mtb;mtb-point-cantor(mtb;y)) m) ≤ ((r(2)/r(n + 1))
+ (r(2)/r(m + 1))))
18. ∀n,m:ℕ.
(mdist(d;mtb-seq(mtb;mtb-point-cantor(mtb;x)) n;mtb-seq(mtb;mtb-point-cantor(mtb;x)) m) ≤ ((r(2)/r(n + 1))
+ (r(2)/r(m + 1))))
19. j : ℕ
20. m : ℕ
⊢ ∀x,y:X.
((mdist(d;x;y) ≤ (r1/r(n + 1)))
⇒ (∀j:ℕn. ∀m:{n...}.
(mdist(d;mtb-seq(mtb;mtb-point-cantor(mtb;x)) j;mtb-seq(mtb;mtb-point-cantor(mtb;y)) m) ≤ ((r(2)/r(j + 1))
+ (r(2)/r(m + 1))))))
2
1. X : Type
2. d : metric(X)
3. cmplt : mcomplete(X with d)
4. mtb : m-TB(X;d)
5. n : ℕ
6. x : X
7. y : X
8. mdist(d;x;y) ≤ (r1/r(n + 1))
9. m-k-regular(d;1;mtb-seq(mtb;mtb-point-cantor(mtb;x)))
10. m-regularize(d;mtb-seq(mtb;mtb-point-cantor(mtb;x))) = mtb-seq(mtb;mtb-point-cantor(mtb;x)) ∈ (ℕ ⟶ X)
11. ∀[s:ℕ ⟶ X]. (λk.(6 * k) ∈ mcauchy(d;n.m-regularize(d;s) n))
12. mtb-cantor(mtb) ⊆r (i:ℕn ⟶ ℕ(fst(mtb)) i)
13. mtb-point-cantor(mtb;x)
= (λi.if i <z n then mtb-point-cantor(mtb;x) i else mtb-point-cantor(mtb;y) i fi )
∈ (i:ℕn ⟶ ℕ(fst(mtb)) i)
14. mtb-cantor-map(d;cmplt;mtb;mtb-point-cantor(mtb;x)) ≡ x
15. m-k-regular(d;1;mtb-seq(mtb;mtb-point-cantor(mtb;y)))
16. ∀[X:Type]. ∀[d:metric(X)]. ∀[s:ℕ ⟶ X]. m-k-regular(d;2;s) supposing m-k-regular(d;1;s)
17. ∀n,m:ℕ.
(mdist(d;mtb-seq(mtb;mtb-point-cantor(mtb;y)) n;mtb-seq(mtb;mtb-point-cantor(mtb;y)) m) ≤ ((r(2)/r(n + 1))
+ (r(2)/r(m + 1))))
18. ∀n,m:ℕ.
(mdist(d;mtb-seq(mtb;mtb-point-cantor(mtb;x)) n;mtb-seq(mtb;mtb-point-cantor(mtb;x)) m) ≤ ((r(2)/r(n + 1))
+ (r(2)/r(m + 1))))
19. j : ℕ
20. m : ℕ
21. ∀x,y:X.
((mdist(d;x;y) ≤ (r1/r(n + 1)))
⇒ (∀j:ℕn. ∀m:{n...}.
(mdist(d;mtb-seq(mtb;mtb-point-cantor(mtb;x)) j;mtb-seq(mtb;mtb-point-cantor(mtb;y)) m) ≤ ((r(2)/r(j + 1))
+ (r(2)/r(m + 1))))))
⊢ mdist(d;mtb-seq(mtb;λi.if i <z n then mtb-point-cantor(mtb;x) i else mtb-point-cantor(mtb;y) i fi )
j;mtb-seq(mtb;λi.if i <z n then mtb-point-cantor(mtb;x) i else mtb-point-cantor(mtb;y) i fi ) m) ≤ ((r(2)/r(j
+ 1))
+ (r(2)/r(m + 1)))
Latex:
Latex:
1. X : Type
2. d : metric(X)
3. cmplt : mcomplete(X with d)
4. mtb : m-TB(X;d)
5. n : \mBbbN{}
6. x : X
7. y : X
8. mdist(d;x;y) \mleq{} (r1/r(n + 1))
9. m-k-regular(d;1;mtb-seq(mtb;mtb-point-cantor(mtb;x)))
10. m-regularize(d;mtb-seq(mtb;mtb-point-cantor(mtb;x))) = mtb-seq(mtb;mtb-point-cantor(mtb;x))
11. \mforall{}[s:\mBbbN{} {}\mrightarrow{} X]. (\mlambda{}k.(6 * k) \mmember{} mcauchy(d;n.m-regularize(d;s) n))
12. mtb-cantor(mtb) \msubseteq{}r (i:\mBbbN{}n {}\mrightarrow{} \mBbbN{}(fst(mtb)) i)
13. mtb-point-cantor(mtb;x)
= (\mlambda{}i.if i <z n then mtb-point-cantor(mtb;x) i else mtb-point-cantor(mtb;y) i fi )
14. mtb-cantor-map(d;cmplt;mtb;mtb-point-cantor(mtb;x)) \mequiv{} x
15. m-k-regular(d;1;mtb-seq(mtb;mtb-point-cantor(mtb;y)))
16. \mforall{}[X:Type]. \mforall{}[d:metric(X)]. \mforall{}[s:\mBbbN{} {}\mrightarrow{} X]. m-k-regular(d;2;s) supposing m-k-regular(d;1;s)
17. \mforall{}n,m:\mBbbN{}.
(mdist(d;mtb-seq(mtb;mtb-point-cantor(mtb;y)) n;mtb-seq(mtb;mtb-point-cantor(mtb;y))
m) \mleq{} ((r(2)/r(n + 1)) + (r(2)/r(m + 1))))
18. \mforall{}n,m:\mBbbN{}.
(mdist(d;mtb-seq(mtb;mtb-point-cantor(mtb;x)) n;mtb-seq(mtb;mtb-point-cantor(mtb;x))
m) \mleq{} ((r(2)/r(n + 1)) + (r(2)/r(m + 1))))
19. j : \mBbbN{}
20. m : \mBbbN{}
\mvdash{} mdist(d;mtb-seq(mtb;...)
j;mtb-seq(mtb;\mlambda{}i.if i <z n
then mtb-point-cantor(mtb;x) i
else mtb-point-cantor(mtb;y) i
fi )
m) \mleq{} ((r(2)/r(j + 1)) + (r(2)/r(m + 1)))
By
Latex:
Assert \mkleeneopen{}\mforall{}x,y:X.
((mdist(d;x;y) \mleq{} (r1/r(n + 1)))
{}\mRightarrow{} (\mforall{}j:\mBbbN{}n. \mforall{}m:\{n...\}.
(mdist(d;mtb-seq(mtb;mtb-point-cantor(mtb;x))
j;mtb-seq(mtb;mtb-point-cantor(mtb;y)) m) \mleq{} ((r(2)/r(j + 1))
+ (r(2)/r(m + 1))))))\mkleeneclose{}\mcdot{}
Home
Index