---

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


1. rv : InnerProductSpace
2. f : Point ⟶ Point
3. r : {r:ℝ| r0 < r} 
4. N : {2...}
5. ∀x,y:Point.  (x ≡ y ⇒ f x ≡ f y)
6. ∀x,y:Point.  ((||x - y|| = r) ⇒ (||f x - f y|| ≤ r))
7. ∀x,y:Point.  ((||x - y|| = (r(N) * r)) ⇒ ((r(N) * r) ≤ ||f x - f y||))
8. ∀x,y:Point.  (((||x - y|| = r) ∨ (||x - y|| = (r(2) * r))) ⇒ (||f x - f y|| = ||x - y||))
9. ∀s,r@0:ℝ.
     ((∃n,m:ℕ+. (s = (r(n)/r(m))))
     ⇒ (∃n,m:ℕ+. (r@0 = (r(n)/r(m))))
     ⇒ (∀x,y:Point.  ((||x - y|| ∈ (r@0 * r, s * r)) ⇒ (||f x - f y|| ∈ [r@0 * r, s * r]))))
10. x : Point
11. y : Point
12. r0 < ||x - y||
⊢ ||f x - f y|| = ||x - y||
BY
{ (BLemma `req-iff-rabs-rleq`
   THEN Auto
   THEN Assert ⌜∃a,b:ℝ
                 ((∃n,m:ℕ+. (a = (r(n)/r(m))))
                 ∧ (∃n,m:ℕ+. (b = (r(n)/r(m))))
                 ∧ (||x - y|| ∈ (a * r, b * r))
                 ∧ (((b * r) - a * r) ≤ (r1/r(m))))⌝⋅) }

1
.....assertion..... 
1. rv : InnerProductSpace
2. f : Point ⟶ Point
3. r : {r:ℝ| r0 < r} 
4. N : {2...}
5. ∀x,y:Point.  (x ≡ y ⇒ f x ≡ f y)
6. ∀x,y:Point.  ((||x - y|| = r) ⇒ (||f x - f y|| ≤ r))
7. ∀x,y:Point.  ((||x - y|| = (r(N) * r)) ⇒ ((r(N) * r) ≤ ||f x - f y||))
8. ∀x,y:Point.  (((||x - y|| = r) ∨ (||x - y|| = (r(2) * r))) ⇒ (||f x - f y|| = ||x - y||))
9. ∀s,r@0:ℝ.
     ((∃n,m:ℕ+. (s = (r(n)/r(m))))
     ⇒ (∃n,m:ℕ+. (r@0 = (r(n)/r(m))))
     ⇒ (∀x,y:Point.  ((||x - y|| ∈ (r@0 * r, s * r)) ⇒ (||f x - f y|| ∈ [r@0 * r, s * r]))))
10. x : Point
11. y : Point
12. r0 < ||x - y||
13. m : ℕ+
⊢ ∃a,b:ℝ
   ((∃n,m:ℕ+. (a = (r(n)/r(m))))
   ∧ (∃n,m:ℕ+. (b = (r(n)/r(m))))
   ∧ (||x - y|| ∈ (a * r, b * r))
   ∧ (((b * r) - a * r) ≤ (r1/r(m))))

2
1. rv : InnerProductSpace
2. f : Point ⟶ Point
3. r : {r:ℝ| r0 < r} 
4. N : {2...}
5. ∀x,y:Point.  (x ≡ y ⇒ f x ≡ f y)
6. ∀x,y:Point.  ((||x - y|| = r) ⇒ (||f x - f y|| ≤ r))
7. ∀x,y:Point.  ((||x - y|| = (r(N) * r)) ⇒ ((r(N) * r) ≤ ||f x - f y||))
8. ∀x,y:Point.  (((||x - y|| = r) ∨ (||x - y|| = (r(2) * r))) ⇒ (||f x - f y|| = ||x - y||))
9. ∀s,r@0:ℝ.
     ((∃n,m:ℕ+. (s = (r(n)/r(m))))
     ⇒ (∃n,m:ℕ+. (r@0 = (r(n)/r(m))))
     ⇒ (∀x,y:Point.  ((||x - y|| ∈ (r@0 * r, s * r)) ⇒ (||f x - f y|| ∈ [r@0 * r, s * r]))))
10. x : Point
11. y : Point
12. r0 < ||x - y||
13. m : ℕ+
14. ∃a,b:ℝ
     ((∃n,m:ℕ+. (a = (r(n)/r(m))))
     ∧ (∃n,m:ℕ+. (b = (r(n)/r(m))))
     ∧ (||x - y|| ∈ (a * r, b * r))
     ∧ (((b * r) - a * r) ≤ (r1/r(m))))
⊢ |||f x - f y|| - ||x - y||| ≤ (r1/r(m))

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  f  :  Point  {}\mrightarrow{}  Point
3.  r  :  \{r:\mBbbR{}|  r0  <  r\} 
4.  N  :  \{2...\}
5.  \mforall{}x,y:Point.    (x  \mequiv{}  y  {}\mRightarrow{}  f  x  \mequiv{}  f  y)
6.  \mforall{}x,y:Point.    ((||x  -  y||  =  r)  {}\mRightarrow{}  (||f  x  -  f  y||  \mleq{}  r))
7.  \mforall{}x,y:Point.    ((||x  -  y||  =  (r(N)  *  r))  {}\mRightarrow{}  ((r(N)  *  r)  \mleq{}  ||f  x  -  f  y||))
8.  \mforall{}x,y:Point.    (((||x  -  y||  =  r)  \mvee{}  (||x  -  y||  =  (r(2)  *  r)))  {}\mRightarrow{}  (||f  x  -  f  y||  =  ||x  -  y||))
9.  \mforall{}s,r@0:\mBbbR{}.
          ((\mexists{}n,m:\mBbbN{}\msupplus{}.  (s  =  (r(n)/r(m))))
          {}\mRightarrow{}  (\mexists{}n,m:\mBbbN{}\msupplus{}.  (r@0  =  (r(n)/r(m))))
          {}\mRightarrow{}  (\mforall{}x,y:Point.    ((||x  -  y||  \mmember{}  (r@0  *  r,  s  *  r))  {}\mRightarrow{}  (||f  x  -  f  y||  \mmember{}  [r@0  *  r,  s  *  r]))))
10.  x  :  Point
11.  y  :  Point
12.  r0  <  ||x  -  y||
\mvdash{}  ||f  x  -  f  y||  =  ||x  -  y||


By

---

Latex:
(BLemma  `req-iff-rabs-rleq`
  THEN  Auto
  THEN  Assert  \mkleeneopen{}\mexists{}a,b:\mBbbR{}
                              ((\mexists{}n,m:\mBbbN{}\msupplus{}.  (a  =  (r(n)/r(m))))
                              \mwedge{}  (\mexists{}n,m:\mBbbN{}\msupplus{}.  (b  =  (r(n)/r(m))))
                              \mwedge{}  (||x  -  y||  \mmember{}  (a  *  r,  b  *  r))
                              \mwedge{}  (((b  *  r)  -  a  *  r)  \mleq{}  (r1/r(m))))\mkleeneclose{}\mcdot{})

---

Home Index