---

Step * 1 1 2 1 1 1 of Lemma implies-isometry-lemma4


1. rv : InnerProductSpace
2. f : Point(rv) ⟶ Point(rv)
3. r : {r:ℝ| r0 < r} 
4. ∀x,y:Point(rv).  (x ≡ y ⇒ f x ≡ f y)
5. ∀x,y:Point(rv).  (((||x - y|| = r) ∨ (||x - y|| = (r(2) * r))) ⇒ (||f x - f y|| = ||x - y||))
6. ∀n,m:ℕ+. ∀x,y:Point(rv).  ((||x - y|| = (r(n) * r/r(m))) ⇒ (||f x - f y|| = ||x - y||))
7. n : ℕ+
8. m : ℕ+
9. x : Point(rv)
10. y : Point(rv)
11. ||x - y|| < (r(n) * r/r(m))
12. r0 < ||x - y||
13. z : Point(rv)
14. ||z - x|| = (r(n) * r/r(2 * m))
15. ||z - y|| = (r(n) * r/r(2 * m))
16. ||f z - f x|| = ||z - x||
17. ||f z - f y|| = ||z - y||
18. ||f x - f y|| ≤ (||f x - f z|| + ||f z - f y||)
19. ||f x - f z|| = ||f z - f x||
⊢ ((r(n) * r) + (r(n) * r)/r(2 * m)) ≤ (r(n) * r/r(m))
BY
{ ((Assert (r(2)/r(2 * m)) ≤ (r1/r(m)) BY
          Auto)
   THEN (Assert ⌜r0 < (r(n) * r)⌝⋅ THENA (Auto THEN All Thin THEN EAuto 2))
   THEN MoveToConcl (-1)
   THEN (GenConclTerm  ⌜r(n) * r⌝⋅ THENA Auto)) }

1
1. rv : InnerProductSpace
2. f : Point(rv) ⟶ Point(rv)
3. r : {r:ℝ| r0 < r} 
4. ∀x,y:Point(rv).  (x ≡ y ⇒ f x ≡ f y)
5. ∀x,y:Point(rv).  (((||x - y|| = r) ∨ (||x - y|| = (r(2) * r))) ⇒ (||f x - f y|| = ||x - y||))
6. ∀n,m:ℕ+. ∀x,y:Point(rv).  ((||x - y|| = (r(n) * r/r(m))) ⇒ (||f x - f y|| = ||x - y||))
7. n : ℕ+
8. m : ℕ+
9. x : Point(rv)
10. y : Point(rv)
11. ||x - y|| < (r(n) * r/r(m))
12. r0 < ||x - y||
13. z : Point(rv)
14. ||z - x|| = (r(n) * r/r(2 * m))
15. ||z - y|| = (r(n) * r/r(2 * m))
16. ||f z - f x|| = ||z - x||
17. ||f z - f y|| = ||z - y||
18. ||f x - f y|| ≤ (||f x - f z|| + ||f z - f y||)
19. ||f x - f z|| = ||f z - f x||
20. (r(2)/r(2 * m)) ≤ (r1/r(m))
21. v : ℝ
22. (r(n) * r) = v ∈ ℝ
⊢ (r0 < v) ⇒ ((v + v/r(2 * m)) ≤ (v/r(m)))

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  f  :  Point(rv)  {}\mrightarrow{}  Point(rv)
3.  r  :  \{r:\mBbbR{}|  r0  <  r\} 
4.  \mforall{}x,y:Point(rv).    (x  \mequiv{}  y  {}\mRightarrow{}  f  x  \mequiv{}  f  y)
5.  \mforall{}x,y:Point(rv).    (((||x  -  y||  =  r)  \mvee{}  (||x  -  y||  =  (r(2)  *  r)))  {}\mRightarrow{}  (||f  x  -  f  y||  =  ||x  -  y||))
6.  \mforall{}n,m:\mBbbN{}\msupplus{}.  \mforall{}x,y:Point(rv).    ((||x  -  y||  =  (r(n)  *  r/r(m)))  {}\mRightarrow{}  (||f  x  -  f  y||  =  ||x  -  y||))
7.  n  :  \mBbbN{}\msupplus{}
8.  m  :  \mBbbN{}\msupplus{}
9.  x  :  Point(rv)
10.  y  :  Point(rv)
11.  ||x  -  y||  <  (r(n)  *  r/r(m))
12.  r0  <  ||x  -  y||
13.  z  :  Point(rv)
14.  ||z  -  x||  =  (r(n)  *  r/r(2  *  m))
15.  ||z  -  y||  =  (r(n)  *  r/r(2  *  m))
16.  ||f  z  -  f  x||  =  ||z  -  x||
17.  ||f  z  -  f  y||  =  ||z  -  y||
18.  ||f  x  -  f  y||  \mleq{}  (||f  x  -  f  z||  +  ||f  z  -  f  y||)
19.  ||f  x  -  f  z||  =  ||f  z  -  f  x||
\mvdash{}  ((r(n)  *  r)  +  (r(n)  *  r)/r(2  *  m))  \mleq{}  (r(n)  *  r/r(m))


By

---

Latex:
((Assert  (r(2)/r(2  *  m))  \mleq{}  (r1/r(m))  BY
                Auto)
  THEN  (Assert  \mkleeneopen{}r0  <  (r(n)  *  r)\mkleeneclose{}\mcdot{}  THENA  (Auto  THEN  All  Thin  THEN  EAuto  2))
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm    \mkleeneopen{}r(n)  *  r\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index