Step
*
1
1
of Lemma
real-ball-uniform-continuity
1. k : ℕ
2. n : ℕ+
3. f : {f:B(n;r1) ⟶ ℝ^k| ∀x,y:B(n;r1). (req-vec(n;x;y) ⇒ req-vec(k;f x;f y))}
4. e : {e:ℝ| r0 < e}
5. f1 : FUN(B(n;r1) ⟶ [r(-1), r1]^n)
6. g : FUN([r(-1), r1]^n ⟶ B(n;r1))
7. ∀x:B(n;r1). g (f1 x) ≡ x
8. ∀y:[r(-1), r1]^n. f1 (g y) ≡ y
9. B : ℕ+
10. ∀x1,x2:B(n;r1). (mdist(max-metric(n);f1 x1;f1 x2) ≤ (r(B) * mdist(rn-metric(n);x1;x2)))
11. ∀f:{f:[r(-1), r1]^n ⟶ ℝ^k| ∀x,y:[r(-1), r1]^n. (req-vec(n;x;y) ⇒ req-vec(k;f x;f y))} . ∀e:{e:ℝ| r0 < e} .
∃d:ℕ+. ∀x,y:[r(-1), r1]^n. ((d(x;y) ≤ (r1/r(d))) ⇒ (d(f x;f y) ≤ e))
12. f o g ∈ {f:[r(-1), r1]^n ⟶ ℝ^k| ∀x,y:[r(-1), r1]^n. (req-vec(n;x;y) ⇒ req-vec(k;f x;f y))}
13. d : ℕ+
14. ∀x,y:[r(-1), r1]^n. ((d(x;y) ≤ (r1/r(d))) ⇒ (d(f (g x);f (g y)) ≤ e))
⊢ ∃d:ℕ+. ∀x,y:B(n;r1). ((d(x;y) ≤ (r1/r(d))) ⇒ (d(f x;f y) ≤ e))
BY
{ Assert ⌜∃d2:ℕ+. ∀x,y:B(n;r1). ((d(x;y) ≤ (r1/r(d2))) ⇒ (d(f1 x;f1 y) ≤ (r1/r(d))))⌝⋅ }
1
.....assertion.....
1. k : ℕ
2. n : ℕ+
3. f : {f:B(n;r1) ⟶ ℝ^k| ∀x,y:B(n;r1). (req-vec(n;x;y) ⇒ req-vec(k;f x;f y))}
4. e : {e:ℝ| r0 < e}
5. f1 : FUN(B(n;r1) ⟶ [r(-1), r1]^n)
6. g : FUN([r(-1), r1]^n ⟶ B(n;r1))
7. ∀x:B(n;r1). g (f1 x) ≡ x
8. ∀y:[r(-1), r1]^n. f1 (g y) ≡ y
9. B : ℕ+
10. ∀x1,x2:B(n;r1). (mdist(max-metric(n);f1 x1;f1 x2) ≤ (r(B) * mdist(rn-metric(n);x1;x2)))
11. ∀f:{f:[r(-1), r1]^n ⟶ ℝ^k| ∀x,y:[r(-1), r1]^n. (req-vec(n;x;y) ⇒ req-vec(k;f x;f y))} . ∀e:{e:ℝ| r0 < e} .
∃d:ℕ+. ∀x,y:[r(-1), r1]^n. ((d(x;y) ≤ (r1/r(d))) ⇒ (d(f x;f y) ≤ e))
12. f o g ∈ {f:[r(-1), r1]^n ⟶ ℝ^k| ∀x,y:[r(-1), r1]^n. (req-vec(n;x;y) ⇒ req-vec(k;f x;f y))}
13. d : ℕ+
14. ∀x,y:[r(-1), r1]^n. ((d(x;y) ≤ (r1/r(d))) ⇒ (d(f (g x);f (g y)) ≤ e))
⊢ ∃d2:ℕ+. ∀x,y:B(n;r1). ((d(x;y) ≤ (r1/r(d2))) ⇒ (d(f1 x;f1 y) ≤ (r1/r(d))))
2
1. k : ℕ
2. n : ℕ+
3. f : {f:B(n;r1) ⟶ ℝ^k| ∀x,y:B(n;r1). (req-vec(n;x;y) ⇒ req-vec(k;f x;f y))}
4. e : {e:ℝ| r0 < e}
5. f1 : FUN(B(n;r1) ⟶ [r(-1), r1]^n)
6. g : FUN([r(-1), r1]^n ⟶ B(n;r1))
7. ∀x:B(n;r1). g (f1 x) ≡ x
8. ∀y:[r(-1), r1]^n. f1 (g y) ≡ y
9. B : ℕ+
10. ∀x1,x2:B(n;r1). (mdist(max-metric(n);f1 x1;f1 x2) ≤ (r(B) * mdist(rn-metric(n);x1;x2)))
11. ∀f:{f:[r(-1), r1]^n ⟶ ℝ^k| ∀x,y:[r(-1), r1]^n. (req-vec(n;x;y) ⇒ req-vec(k;f x;f y))} . ∀e:{e:ℝ| r0 < e} .
∃d:ℕ+. ∀x,y:[r(-1), r1]^n. ((d(x;y) ≤ (r1/r(d))) ⇒ (d(f x;f y) ≤ e))
12. f o g ∈ {f:[r(-1), r1]^n ⟶ ℝ^k| ∀x,y:[r(-1), r1]^n. (req-vec(n;x;y) ⇒ req-vec(k;f x;f y))}
13. d : ℕ+
14. ∀x,y:[r(-1), r1]^n. ((d(x;y) ≤ (r1/r(d))) ⇒ (d(f (g x);f (g y)) ≤ e))
15. ∃d2:ℕ+. ∀x,y:B(n;r1). ((d(x;y) ≤ (r1/r(d2))) ⇒ (d(f1 x;f1 y) ≤ (r1/r(d))))
⊢ ∃d:ℕ+. ∀x,y:B(n;r1). ((d(x;y) ≤ (r1/r(d))) ⇒ (d(f x;f y) ≤ e))
Latex:
Latex:
1. k : \mBbbN{}
2. n : \mBbbN{}\msupplus{}
3. f : \{f:B(n;r1) {}\mrightarrow{} \mBbbR{}\^{}k| \mforall{}x,y:B(n;r1). (req-vec(n;x;y) {}\mRightarrow{} req-vec(k;f x;f y))\}
4. e : \{e:\mBbbR{}| r0 < e\}
5. f1 : FUN(B(n;r1) {}\mrightarrow{} [r(-1), r1]\^{}n)
6. g : FUN([r(-1), r1]\^{}n {}\mrightarrow{} B(n;r1))
7. \mforall{}x:B(n;r1). g (f1 x) \mequiv{} x
8. \mforall{}y:[r(-1), r1]\^{}n. f1 (g y) \mequiv{} y
9. B : \mBbbN{}\msupplus{}
10. \mforall{}x1,x2:B(n;r1). (mdist(max-metric(n);f1 x1;f1 x2) \mleq{} (r(B) * mdist(rn-metric(n);x1;x2)))
11. \mforall{}f:\{f:[r(-1), r1]\^{}n {}\mrightarrow{} \mBbbR{}\^{}k| \mforall{}x,y:[r(-1), r1]\^{}n. (req-vec(n;x;y) {}\mRightarrow{} req-vec(k;f x;f y))\} .
\mforall{}e:\{e:\mBbbR{}| r0 < e\} .
\mexists{}d:\mBbbN{}\msupplus{}. \mforall{}x,y:[r(-1), r1]\^{}n. ((d(x;y) \mleq{} (r1/r(d))) {}\mRightarrow{} (d(f x;f y) \mleq{} e))
12. f o g \mmember{} \{f:[r(-1), r1]\^{}n {}\mrightarrow{} \mBbbR{}\^{}k| \mforall{}x,y:[r(-1), r1]\^{}n. (req-vec(n;x;y) {}\mRightarrow{} req-vec(k;f x;f y))\}
13. d : \mBbbN{}\msupplus{}
14. \mforall{}x,y:[r(-1), r1]\^{}n. ((d(x;y) \mleq{} (r1/r(d))) {}\mRightarrow{} (d(f (g x);f (g y)) \mleq{} e))
\mvdash{} \mexists{}d:\mBbbN{}\msupplus{}. \mforall{}x,y:B(n;r1). ((d(x;y) \mleq{} (r1/r(d))) {}\mRightarrow{} (d(f x;f y) \mleq{} e))
By
Latex:
Assert \mkleeneopen{}\mexists{}d2:\mBbbN{}\msupplus{}. \mforall{}x,y:B(n;r1). ((d(x;y) \mleq{} (r1/r(d2))) {}\mRightarrow{} (d(f1 x;f1 y) \mleq{} (r1/r(d))))\mkleeneclose{}\mcdot{}
Home
Index