Step
*
2
2
2
2
5
2
of Lemma
unit-ball-to-unit-cube
1. n : ℕ+
2. λi.r0 ∈ ℝ^n
3. max-metric(n) ≤ rn-metric(n)
4. rn-metric(n) ≤ r(n)*max-metric(n)
5. ∀p:ℝ^n. (r0 < ||p|| ⇐⇒ r0 < mdist(max-metric(n);λi.r0;p))
6. ∀p:{p:ℝ^n| r0 < mdist(max-metric(n);p;λi.r0)} . ((||p||/mdist(max-metric(n);p;λi.r0))*p ∈ ℝ^n)
7. h : ℝ^n ⟶ ℝ^n
8. ∀p:ℝ^n. (req-vec(n;p;λi.r0) ⇒ h p ≡ λi.r0)
9. ∀p:{p:ℝ^n| r0 < mdist(max-metric(n);p;λi.r0)} . h p ≡ (||p||/mdist(max-metric(n);p;λi.r0))*p
10. λp.(||p||/mdist(max-metric(n);p;λi.r0))*p:FUN({p:ℝ^n| r0 < mdist(max-metric(n);p;λi.r0)} ;ℝ^n) ⇒ h:FUN(ℝ^n;ℝ^n)
11. h ∈ {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1} ⟶ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1}
12. ∀p:ℝ^n. (req-vec(n;p;λi.r0) ⇒ h p ≡ λi.r0)
13. ∀p:{p:ℝ^n| r0 < mdist(max-metric(n);λi.r0;p)} . h p ≡ (λp.(||p||/mdist(max-metric(n);p;λi.r0))*p) p
14. h ∈ {p:ℝ^n| ||p|| ≤ r1} ⟶ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1}
15. h:FUN(ℝ^n;ℝ^n)
16. x : {p:ℝ^n| ||p|| ≤ r1}
17. y : {p:ℝ^n| ||p|| ≤ r1}
18. ∀x,y:{p:ℝ^n| (||p|| ≤ r1) ∧ (r0 < mdist(max-metric(n);p;λi.r0))} .
((|(||x||/mdist(max-metric(n);x;λi.r0)) - (||y||/mdist(max-metric(n);y;λi.r0))|
* mdist(max-metric(n);x;λi.r0)) ≤ (r(n + 1) * mdist(rn-metric(n);x;y)))
⊢ mdist(max-metric(n);h x;h y) ≤ (r((2 * n) + 1) * mdist(rn-metric(n);x;y))
BY
{ (Thin (-5)
THEN Thin (-7)
THEN D -3
THEN D -2
THEN ((StableCases ⌜r0 < mdist(max-metric(n);x;λi.r0)⌝⋅ THENA Auto)
THENL [((InstHyp [⌜x⌝] 9⋅ THENA Auto)
THEN (RWO "-1" 0 THENA Auto)
THEN (GenConcl ⌜(||x||/mdist(max-metric(n);x;λi.r0)) = c ∈ {c:ℝ| (r0 ≤ c) ∧ (c ≤ r(n))} ⌝⋅
THENA (Auto
THEN MemTypeCD
THEN Auto
THEN nRMul ⌜mdist(max-metric(n);x;λi.r0)⌝ 0⋅
THEN Auto
THEN (D 4 With ⌜x⌝ THENA Auto)
THEN (D -1 With ⌜λi.r0⌝ THENA Auto)
THEN RepUR ``mdist scale-metric rn-metric`` -1
THEN Fold `mdist` (-1)
THEN (RWO "-1<" 0 THENA Auto)
THEN RWO "real-vec-dist-from-zero" 0
THEN Auto)
))
; ((FLemma `not-rless` [-1] THENA Auto)
THEN (Assert mdist(max-metric(n);x;λi.r0) = r0 BY
(BLemma `rleq_antisymmetry` THEN Auto))
THEN (Unfold `mdist` -1 THEN Fold `meq` (-1))
THEN RWO "meq-max-metric" (-1)
THEN Auto
THEN (InstHyp [⌜x⌝] 8⋅ THENA Auto)
THEN (RWO "-1" 0 THENA Auto))]
)
THEN ((StableCases ⌜r0 < mdist(max-metric(n);y;λi.r0)⌝⋅ THENA Auto)
THENL [((InstHyp [⌜y⌝] 9⋅ THENA Auto)
THEN (RWO "-1" 0 THENA Auto)
THEN (GenConcl ⌜(||y||/mdist(max-metric(n);y;λi.r0)) = c' ∈ {c:ℝ| (r0 ≤ c) ∧ (c ≤ r(n))} ⌝⋅
THENA (Auto
THEN MemTypeCD
THEN Auto
THEN nRMul ⌜mdist(max-metric(n);y;λi.r0)⌝ 0⋅
THEN Auto
THEN (D 4 With ⌜y⌝ THENA Auto)
THEN (D -1 With ⌜λi.r0⌝ THENA Auto)
THEN RepUR ``mdist scale-metric rn-metric`` -1
THEN Fold `mdist` (-1)
THEN (RWO "-1<" 0 THENA Auto)
THEN RWO "real-vec-dist-from-zero" 0
THEN Auto)
))
; ((FLemma `not-rless` [-1] THENA Auto)
THEN (Assert mdist(max-metric(n);y;λi.r0) = r0 BY
(BLemma `rleq_antisymmetry` THEN Auto))
THEN (Unfold `mdist` -1 THEN Fold `meq` (-1))
THEN RWO "meq-max-metric" (-1)
THEN Auto
THEN (InstHyp [⌜y⌝] 8⋅ THENA Auto)
THEN (RWO "-1" 0 THENA Auto))]
)) }
1
1. n : ℕ+
2. λi.r0 ∈ ℝ^n
3. max-metric(n) ≤ rn-metric(n)
4. rn-metric(n) ≤ r(n)*max-metric(n)
5. ∀p:ℝ^n. (r0 < ||p|| ⇐⇒ r0 < mdist(max-metric(n);λi.r0;p))
6. ∀p:{p:ℝ^n| r0 < mdist(max-metric(n);p;λi.r0)} . ((||p||/mdist(max-metric(n);p;λi.r0))*p ∈ ℝ^n)
7. h : ℝ^n ⟶ ℝ^n
8. ∀p:ℝ^n. (req-vec(n;p;λi.r0) ⇒ h p ≡ λi.r0)
9. ∀p:{p:ℝ^n| r0 < mdist(max-metric(n);p;λi.r0)} . h p ≡ (||p||/mdist(max-metric(n);p;λi.r0))*p
10. λp.(||p||/mdist(max-metric(n);p;λi.r0))*p:FUN({p:ℝ^n| r0 < mdist(max-metric(n);p;λi.r0)} ;ℝ^n) ⇒ h:FUN(ℝ^n;ℝ^n)
11. ∀p:ℝ^n. (req-vec(n;p;λi.r0) ⇒ h p ≡ λi.r0)
12. ∀p:{p:ℝ^n| r0 < mdist(max-metric(n);λi.r0;p)} . h p ≡ (λp.(||p||/mdist(max-metric(n);p;λi.r0))*p) p
13. h:FUN(ℝ^n;ℝ^n)
14. x : ℝ^n
15. ||x|| ≤ r1
16. y : ℝ^n
17. ||y|| ≤ r1
18. ∀x,y:{p:ℝ^n| (||p|| ≤ r1) ∧ (r0 < mdist(max-metric(n);p;λi.r0))} .
((|(||x||/mdist(max-metric(n);x;λi.r0)) - (||y||/mdist(max-metric(n);y;λi.r0))|
* mdist(max-metric(n);x;λi.r0)) ≤ (r(n + 1) * mdist(rn-metric(n);x;y)))
19. r0 < mdist(max-metric(n);x;λi.r0)
20. h x ≡ (||x||/mdist(max-metric(n);x;λi.r0))*x
21. c : {c:ℝ| (r0 ≤ c) ∧ (c ≤ r(n))}
22. (||x||/mdist(max-metric(n);x;λi.r0)) = c ∈ {c:ℝ| (r0 ≤ c) ∧ (c ≤ r(n))}
23. r0 < mdist(max-metric(n);y;λi.r0)
24. h y ≡ (||y||/mdist(max-metric(n);y;λi.r0))*y
25. c' : {c:ℝ| (r0 ≤ c) ∧ (c ≤ r(n))}
26. (||y||/mdist(max-metric(n);y;λi.r0)) = c' ∈ {c:ℝ| (r0 ≤ c) ∧ (c ≤ r(n))}
⊢ mdist(max-metric(n);c*x;c'*y) ≤ (r((2 * n) + 1) * mdist(rn-metric(n);x;y))
2
1. n : ℕ+
2. λi.r0 ∈ ℝ^n
3. max-metric(n) ≤ rn-metric(n)
4. rn-metric(n) ≤ r(n)*max-metric(n)
5. ∀p:ℝ^n. (r0 < ||p|| ⇐⇒ r0 < mdist(max-metric(n);λi.r0;p))
6. ∀p:{p:ℝ^n| r0 < mdist(max-metric(n);p;λi.r0)} . ((||p||/mdist(max-metric(n);p;λi.r0))*p ∈ ℝ^n)
7. h : ℝ^n ⟶ ℝ^n
8. ∀p:ℝ^n. (req-vec(n;p;λi.r0) ⇒ h p ≡ λi.r0)
9. ∀p:{p:ℝ^n| r0 < mdist(max-metric(n);p;λi.r0)} . h p ≡ (||p||/mdist(max-metric(n);p;λi.r0))*p
10. λp.(||p||/mdist(max-metric(n);p;λi.r0))*p:FUN({p:ℝ^n| r0 < mdist(max-metric(n);p;λi.r0)} ;ℝ^n) ⇒ h:FUN(ℝ^n;ℝ^n)
11. ∀p:ℝ^n. (req-vec(n;p;λi.r0) ⇒ h p ≡ λi.r0)
12. ∀p:{p:ℝ^n| r0 < mdist(max-metric(n);λi.r0;p)} . h p ≡ (λp.(||p||/mdist(max-metric(n);p;λi.r0))*p) p
13. h:FUN(ℝ^n;ℝ^n)
14. x : ℝ^n
15. ||x|| ≤ r1
16. y : ℝ^n
17. ||y|| ≤ r1
18. ∀x,y:{p:ℝ^n| (||p|| ≤ r1) ∧ (r0 < mdist(max-metric(n);p;λi.r0))} .
((|(||x||/mdist(max-metric(n);x;λi.r0)) - (||y||/mdist(max-metric(n);y;λi.r0))|
* mdist(max-metric(n);x;λi.r0)) ≤ (r(n + 1) * mdist(rn-metric(n);x;y)))
19. r0 < mdist(max-metric(n);x;λi.r0)
20. h x ≡ (||x||/mdist(max-metric(n);x;λi.r0))*x
21. c : {c:ℝ| (r0 ≤ c) ∧ (c ≤ r(n))}
22. (||x||/mdist(max-metric(n);x;λi.r0)) = c ∈ {c:ℝ| (r0 ≤ c) ∧ (c ≤ r(n))}
23. ¬(r0 < mdist(max-metric(n);y;λi.r0))
24. mdist(max-metric(n);y;λi.r0) ≤ r0
25. req-vec(n;y;λi.r0)
26. h y ≡ λi.r0
⊢ mdist(max-metric(n);c*x;λi.r0) ≤ (r((2 * n) + 1) * mdist(rn-metric(n);x;y))
3
1. n : ℕ+
2. λi.r0 ∈ ℝ^n
3. max-metric(n) ≤ rn-metric(n)
4. rn-metric(n) ≤ r(n)*max-metric(n)
5. ∀p:ℝ^n. (r0 < ||p|| ⇐⇒ r0 < mdist(max-metric(n);λi.r0;p))
6. ∀p:{p:ℝ^n| r0 < mdist(max-metric(n);p;λi.r0)} . ((||p||/mdist(max-metric(n);p;λi.r0))*p ∈ ℝ^n)
7. h : ℝ^n ⟶ ℝ^n
8. ∀p:ℝ^n. (req-vec(n;p;λi.r0) ⇒ h p ≡ λi.r0)
9. ∀p:{p:ℝ^n| r0 < mdist(max-metric(n);p;λi.r0)} . h p ≡ (||p||/mdist(max-metric(n);p;λi.r0))*p
10. λp.(||p||/mdist(max-metric(n);p;λi.r0))*p:FUN({p:ℝ^n| r0 < mdist(max-metric(n);p;λi.r0)} ;ℝ^n) ⇒ h:FUN(ℝ^n;ℝ^n)
11. ∀p:ℝ^n. (req-vec(n;p;λi.r0) ⇒ h p ≡ λi.r0)
12. ∀p:{p:ℝ^n| r0 < mdist(max-metric(n);λi.r0;p)} . h p ≡ (λp.(||p||/mdist(max-metric(n);p;λi.r0))*p) p
13. h:FUN(ℝ^n;ℝ^n)
14. x : ℝ^n
15. ||x|| ≤ r1
16. y : ℝ^n
17. ||y|| ≤ r1
18. ∀x,y:{p:ℝ^n| (||p|| ≤ r1) ∧ (r0 < mdist(max-metric(n);p;λi.r0))} .
((|(||x||/mdist(max-metric(n);x;λi.r0)) - (||y||/mdist(max-metric(n);y;λi.r0))|
* mdist(max-metric(n);x;λi.r0)) ≤ (r(n + 1) * mdist(rn-metric(n);x;y)))
19. ¬(r0 < mdist(max-metric(n);x;λi.r0))
20. mdist(max-metric(n);x;λi.r0) ≤ r0
21. req-vec(n;x;λi.r0)
22. h x ≡ λi.r0
23. r0 < mdist(max-metric(n);y;λi.r0)
24. h y ≡ (||y||/mdist(max-metric(n);y;λi.r0))*y
25. c' : {c:ℝ| (r0 ≤ c) ∧ (c ≤ r(n))}
26. (||y||/mdist(max-metric(n);y;λi.r0)) = c' ∈ {c:ℝ| (r0 ≤ c) ∧ (c ≤ r(n))}
⊢ mdist(max-metric(n);λi.r0;c'*y) ≤ (r((2 * n) + 1) * mdist(rn-metric(n);x;y))
4
1. n : ℕ+
2. λi.r0 ∈ ℝ^n
3. max-metric(n) ≤ rn-metric(n)
4. rn-metric(n) ≤ r(n)*max-metric(n)
5. ∀p:ℝ^n. (r0 < ||p|| ⇐⇒ r0 < mdist(max-metric(n);λi.r0;p))
6. ∀p:{p:ℝ^n| r0 < mdist(max-metric(n);p;λi.r0)} . ((||p||/mdist(max-metric(n);p;λi.r0))*p ∈ ℝ^n)
7. h : ℝ^n ⟶ ℝ^n
8. ∀p:ℝ^n. (req-vec(n;p;λi.r0) ⇒ h p ≡ λi.r0)
9. ∀p:{p:ℝ^n| r0 < mdist(max-metric(n);p;λi.r0)} . h p ≡ (||p||/mdist(max-metric(n);p;λi.r0))*p
10. λp.(||p||/mdist(max-metric(n);p;λi.r0))*p:FUN({p:ℝ^n| r0 < mdist(max-metric(n);p;λi.r0)} ;ℝ^n) ⇒ h:FUN(ℝ^n;ℝ^n)
11. ∀p:ℝ^n. (req-vec(n;p;λi.r0) ⇒ h p ≡ λi.r0)
12. ∀p:{p:ℝ^n| r0 < mdist(max-metric(n);λi.r0;p)} . h p ≡ (λp.(||p||/mdist(max-metric(n);p;λi.r0))*p) p
13. h:FUN(ℝ^n;ℝ^n)
14. x : ℝ^n
15. ||x|| ≤ r1
16. y : ℝ^n
17. ||y|| ≤ r1
18. ∀x,y:{p:ℝ^n| (||p|| ≤ r1) ∧ (r0 < mdist(max-metric(n);p;λi.r0))} .
((|(||x||/mdist(max-metric(n);x;λi.r0)) - (||y||/mdist(max-metric(n);y;λi.r0))|
* mdist(max-metric(n);x;λi.r0)) ≤ (r(n + 1) * mdist(rn-metric(n);x;y)))
19. ¬(r0 < mdist(max-metric(n);x;λi.r0))
20. mdist(max-metric(n);x;λi.r0) ≤ r0
21. req-vec(n;x;λi.r0)
22. h x ≡ λi.r0
23. ¬(r0 < mdist(max-metric(n);y;λi.r0))
24. mdist(max-metric(n);y;λi.r0) ≤ r0
25. req-vec(n;y;λi.r0)
26. h y ≡ λi.r0
⊢ mdist(max-metric(n);λi.r0;λi.r0) ≤ (r((2 * n) + 1) * mdist(rn-metric(n);x;y))
Latex:
Latex:
1. n : \mBbbN{}\msupplus{}
2. \mlambda{}i.r0 \mmember{} \mBbbR{}\^{}n
3. max-metric(n) \mleq{} rn-metric(n)
4. rn-metric(n) \mleq{} r(n)*max-metric(n)
5. \mforall{}p:\mBbbR{}\^{}n. (r0 < ||p|| \mLeftarrow{}{}\mRightarrow{} r0 < mdist(max-metric(n);\mlambda{}i.r0;p))
6. \mforall{}p:\{p:\mBbbR{}\^{}n| r0 < mdist(max-metric(n);p;\mlambda{}i.r0)\} . ((||p||/mdist(max-metric(n);p;\mlambda{}i.r0))*p \mmember{} \mBbbR{}\^{}n)
7. h : \mBbbR{}\^{}n {}\mrightarrow{} \mBbbR{}\^{}n
8. \mforall{}p:\mBbbR{}\^{}n. (req-vec(n;p;\mlambda{}i.r0) {}\mRightarrow{} h p \mequiv{} \mlambda{}i.r0)
9. \mforall{}p:\{p:\mBbbR{}\^{}n| r0 < mdist(max-metric(n);p;\mlambda{}i.r0)\} . h p \mequiv{} (||p||/mdist(max-metric(n);p;\mlambda{}i.r0))*p
10. \mlambda{}p.(||p||/mdist(max-metric(n);p;\mlambda{}i.r0))*p:FUN(\{p:\mBbbR{}\^{}n| r0 < mdist(max-metric(n);p;\mlambda{}i.r0)\} ;\mBbbR{}\^{}n) {}\000C\mRightarrow{} h:FUN(\mBbbR{}\^{}n;\mBbbR{}\^{}n)
11. h \mmember{} \{q:\mBbbR{}\^{}n| mdist(rn-metric(n);\mlambda{}i.r0;q) \mleq{} r1\} {}\mrightarrow{} \{q:\mBbbR{}\^{}n| mdist(max-metric(n);\mlambda{}i.r0;q) \mleq{} r1\}
12. \mforall{}p:\mBbbR{}\^{}n. (req-vec(n;p;\mlambda{}i.r0) {}\mRightarrow{} h p \mequiv{} \mlambda{}i.r0)
13. \mforall{}p:\{p:\mBbbR{}\^{}n| r0 < mdist(max-metric(n);\mlambda{}i.r0;p)\}
h p \mequiv{} (\mlambda{}p.(||p||/mdist(max-metric(n);p;\mlambda{}i.r0))*p) p
14. h \mmember{} \{p:\mBbbR{}\^{}n| ||p|| \mleq{} r1\} {}\mrightarrow{} \{q:\mBbbR{}\^{}n| mdist(max-metric(n);\mlambda{}i.r0;q) \mleq{} r1\}
15. h:FUN(\mBbbR{}\^{}n;\mBbbR{}\^{}n)
16. x : \{p:\mBbbR{}\^{}n| ||p|| \mleq{} r1\}
17. y : \{p:\mBbbR{}\^{}n| ||p|| \mleq{} r1\}
18. \mforall{}x,y:\{p:\mBbbR{}\^{}n| (||p|| \mleq{} r1) \mwedge{} (r0 < mdist(max-metric(n);p;\mlambda{}i.r0))\} .
((|(||x||/mdist(max-metric(n);x;\mlambda{}i.r0)) - (||y||/mdist(max-metric(n);y;\mlambda{}i.r0))|
* mdist(max-metric(n);x;\mlambda{}i.r0)) \mleq{} (r(n + 1) * mdist(rn-metric(n);x;y)))
\mvdash{} mdist(max-metric(n);h x;h y) \mleq{} (r((2 * n) + 1) * mdist(rn-metric(n);x;y))
By
Latex:
(Thin (-5)
THEN Thin (-7)
THEN D -3
THEN D -2
THEN ((StableCases \mkleeneopen{}r0 < mdist(max-metric(n);x;\mlambda{}i.r0)\mkleeneclose{}\mcdot{} THENA Auto)
THENL [((InstHyp [\mkleeneopen{}x\mkleeneclose{}] 9\mcdot{} THENA Auto)
THEN (RWO "-1" 0 THENA Auto)
THEN (GenConcl \mkleeneopen{}(||x||/mdist(max-metric(n);x;\mlambda{}i.r0)) = c\mkleeneclose{}\mcdot{}
THENA (Auto
THEN MemTypeCD
THEN Auto
THEN nRMul \mkleeneopen{}mdist(max-metric(n);x;\mlambda{}i.r0)\mkleeneclose{} 0\mcdot{}
THEN Auto
THEN (D 4 With \mkleeneopen{}x\mkleeneclose{} THENA Auto)
THEN (D -1 With \mkleeneopen{}\mlambda{}i.r0\mkleeneclose{} THENA Auto)
THEN RepUR ``mdist scale-metric rn-metric`` -1
THEN Fold `mdist` (-1)
THEN (RWO "-1<" 0 THENA Auto)
THEN RWO "real-vec-dist-from-zero" 0
THEN Auto)
))
; ((FLemma `not-rless` [-1] THENA Auto)
THEN (Assert mdist(max-metric(n);x;\mlambda{}i.r0) = r0 BY
(BLemma `rleq\_antisymmetry` THEN Auto))
THEN (Unfold `mdist` -1 THEN Fold `meq` (-1))
THEN RWO "meq-max-metric" (-1)
THEN Auto
THEN (InstHyp [\mkleeneopen{}x\mkleeneclose{}] 8\mcdot{} THENA Auto)
THEN (RWO "-1" 0 THENA Auto))]
)
THEN ((StableCases \mkleeneopen{}r0 < mdist(max-metric(n);y;\mlambda{}i.r0)\mkleeneclose{}\mcdot{} THENA Auto)
THENL [((InstHyp [\mkleeneopen{}y\mkleeneclose{}] 9\mcdot{} THENA Auto)
THEN (RWO "-1" 0 THENA Auto)
THEN (GenConcl \mkleeneopen{}(||y||/mdist(max-metric(n);y;\mlambda{}i.r0)) = c'\mkleeneclose{}\mcdot{}
THENA (Auto
THEN MemTypeCD
THEN Auto
THEN nRMul \mkleeneopen{}mdist(max-metric(n);y;\mlambda{}i.r0)\mkleeneclose{} 0\mcdot{}
THEN Auto
THEN (D 4 With \mkleeneopen{}y\mkleeneclose{} THENA Auto)
THEN (D -1 With \mkleeneopen{}\mlambda{}i.r0\mkleeneclose{} THENA Auto)
THEN RepUR ``mdist scale-metric rn-metric`` -1
THEN Fold `mdist` (-1)
THEN (RWO "-1<" 0 THENA Auto)
THEN RWO "real-vec-dist-from-zero" 0
THEN Auto)
))
; ((FLemma `not-rless` [-1] THENA Auto)
THEN (Assert mdist(max-metric(n);y;\mlambda{}i.r0) = r0 BY
(BLemma `rleq\_antisymmetry` THEN Auto))
THEN (Unfold `mdist` -1 THEN Fold `meq` (-1))
THEN RWO "meq-max-metric" (-1)
THEN Auto
THEN (InstHyp [\mkleeneopen{}y\mkleeneclose{}] 8\mcdot{} THENA Auto)
THEN (RWO "-1" 0 THENA Auto))]
))
Home
Index