Step
*
1
1
2
1
2
2
of Lemma
implies-isometry-lemma1
1. rv : InnerProductSpace
2. f : Point(rv) ⟶ Point(rv)
3. r : {r:ℝ| r0 < r}
4. N : {2...}
5. ∀x,y:Point(rv). (x ≡ y ⇒ f x ≡ f y)
6. ∀x,y:Point(rv). ((||x - y|| = r) ⇒ (||f x - f y|| ≤ r))
7. ∀x,y:Point(rv). ((||x - y|| = (r(N) * r)) ⇒ ((r(N) * r) ≤ ||f x - f y||))
8. x : Point(rv)
9. y : Point(rv)
10. z : Point(rv)
11. y ≡ (r1/r(2))*x + z ∧ (||x - y|| = r) ∧ (||x - z|| = (r(2) * r))
12. ∀i:ℕ. (||x + (r(i)/r(2))*z - x - x + (r(i + 1)/r(2))*z - x|| = r)
13. ∀i:ℕ. (||f x + (r(i)/r(2))*z - x - f x + (r(i + 1)/r(2))*z - x|| ≤ r)
14. (r(N) * r) ≤ ||f x + (r0/r(2))*z - x - f x + (r(N)/r(2))*z - x||
15. ∀p:ℕ ⟶ Point(rv)
((∀i:ℕ. (||p i - p (i + 1)|| ≤ r))
⇒ ((r(N) * r) ≤ ||p 0 - p N||)
⇒ ((||p 0 - p 1|| = r) ∧ (||p 0 - p 2|| = (r(2) * r))))
⊢ (||f x - f y|| = r) ∧ (||f x - f z|| = (r(2) * r))
BY
{ Assert ⌜f x + (r0/r(2))*z - x ≡ f x ∧ f x + (r1/r(2))*z - x ≡ f y ∧ f x + (r(2)/r(2))*z - x ≡ f z⌝⋅ }
1
.....assertion.....
1. rv : InnerProductSpace
2. f : Point(rv) ⟶ Point(rv)
3. r : {r:ℝ| r0 < r}
4. N : {2...}
5. ∀x,y:Point(rv). (x ≡ y ⇒ f x ≡ f y)
6. ∀x,y:Point(rv). ((||x - y|| = r) ⇒ (||f x - f y|| ≤ r))
7. ∀x,y:Point(rv). ((||x - y|| = (r(N) * r)) ⇒ ((r(N) * r) ≤ ||f x - f y||))
8. x : Point(rv)
9. y : Point(rv)
10. z : Point(rv)
11. y ≡ (r1/r(2))*x + z ∧ (||x - y|| = r) ∧ (||x - z|| = (r(2) * r))
12. ∀i:ℕ. (||x + (r(i)/r(2))*z - x - x + (r(i + 1)/r(2))*z - x|| = r)
13. ∀i:ℕ. (||f x + (r(i)/r(2))*z - x - f x + (r(i + 1)/r(2))*z - x|| ≤ r)
14. (r(N) * r) ≤ ||f x + (r0/r(2))*z - x - f x + (r(N)/r(2))*z - x||
15. ∀p:ℕ ⟶ Point(rv)
((∀i:ℕ. (||p i - p (i + 1)|| ≤ r))
⇒ ((r(N) * r) ≤ ||p 0 - p N||)
⇒ ((||p 0 - p 1|| = r) ∧ (||p 0 - p 2|| = (r(2) * r))))
⊢ f x + (r0/r(2))*z - x ≡ f x ∧ f x + (r1/r(2))*z - x ≡ f y ∧ f x + (r(2)/r(2))*z - x ≡ f z
2
1. rv : InnerProductSpace
2. f : Point(rv) ⟶ Point(rv)
3. r : {r:ℝ| r0 < r}
4. N : {2...}
5. ∀x,y:Point(rv). (x ≡ y ⇒ f x ≡ f y)
6. ∀x,y:Point(rv). ((||x - y|| = r) ⇒ (||f x - f y|| ≤ r))
7. ∀x,y:Point(rv). ((||x - y|| = (r(N) * r)) ⇒ ((r(N) * r) ≤ ||f x - f y||))
8. x : Point(rv)
9. y : Point(rv)
10. z : Point(rv)
11. y ≡ (r1/r(2))*x + z ∧ (||x - y|| = r) ∧ (||x - z|| = (r(2) * r))
12. ∀i:ℕ. (||x + (r(i)/r(2))*z - x - x + (r(i + 1)/r(2))*z - x|| = r)
13. ∀i:ℕ. (||f x + (r(i)/r(2))*z - x - f x + (r(i + 1)/r(2))*z - x|| ≤ r)
14. (r(N) * r) ≤ ||f x + (r0/r(2))*z - x - f x + (r(N)/r(2))*z - x||
15. ∀p:ℕ ⟶ Point(rv)
((∀i:ℕ. (||p i - p (i + 1)|| ≤ r))
⇒ ((r(N) * r) ≤ ||p 0 - p N||)
⇒ ((||p 0 - p 1|| = r) ∧ (||p 0 - p 2|| = (r(2) * r))))
16. f x + (r0/r(2))*z - x ≡ f x ∧ f x + (r1/r(2))*z - x ≡ f y ∧ f x + (r(2)/r(2))*z - x ≡ f z
⊢ (||f x - f y|| = r) ∧ (||f x - f z|| = (r(2) * r))
Latex:
Latex:
1. rv : InnerProductSpace
2. f : Point(rv) {}\mrightarrow{} Point(rv)
3. r : \{r:\mBbbR{}| r0 < r\}
4. N : \{2...\}
5. \mforall{}x,y:Point(rv). (x \mequiv{} y {}\mRightarrow{} f x \mequiv{} f y)
6. \mforall{}x,y:Point(rv). ((||x - y|| = r) {}\mRightarrow{} (||f x - f y|| \mleq{} r))
7. \mforall{}x,y:Point(rv). ((||x - y|| = (r(N) * r)) {}\mRightarrow{} ((r(N) * r) \mleq{} ||f x - f y||))
8. x : Point(rv)
9. y : Point(rv)
10. z : Point(rv)
11. y \mequiv{} (r1/r(2))*x + z \mwedge{} (||x - y|| = r) \mwedge{} (||x - z|| = (r(2) * r))
12. \mforall{}i:\mBbbN{}. (||x + (r(i)/r(2))*z - x - x + (r(i + 1)/r(2))*z - x|| = r)
13. \mforall{}i:\mBbbN{}. (||f x + (r(i)/r(2))*z - x - f x + (r(i + 1)/r(2))*z - x|| \mleq{} r)
14. (r(N) * r) \mleq{} ||f x + (r0/r(2))*z - x - f x + (r(N)/r(2))*z - x||
15. \mforall{}p:\mBbbN{} {}\mrightarrow{} Point(rv)
((\mforall{}i:\mBbbN{}. (||p i - p (i + 1)|| \mleq{} r))
{}\mRightarrow{} ((r(N) * r) \mleq{} ||p 0 - p N||)
{}\mRightarrow{} ((||p 0 - p 1|| = r) \mwedge{} (||p 0 - p 2|| = (r(2) * r))))
\mvdash{} (||f x - f y|| = r) \mwedge{} (||f x - f z|| = (r(2) * r))
By
Latex:
Assert \mkleeneopen{}f x + (r0/r(2))*z - x \mequiv{} f x \mwedge{} f x + (r1/r(2))*z - x \mequiv{} f y \mwedge{} f x + (r(2)/r(2))*z - x \mequiv{} f z\mkleeneclose{}\mcdot{}
Home
Index