---

Step * of Lemma implies-isometry-lemma4

No Annotations
∀rv:InnerProductSpace. ∀f:Point(rv) ⟶ Point(rv). ∀r:{r:ℝ| r0 < r} .
  ((∀x,y:Point(rv).  (x ≡ y ⇒ f x ≡ f y))
  ⇒ (∀x,y:Point(rv).  (((||x - y|| = r) ∨ (||x - y|| = (r(2) * r))) ⇒ (||f x - f y|| = ||x - y||)))
  ⇒ (∀n,m:ℕ+. ∀x,y:Point(rv).  ((||x - y|| < (r(n) * r/r(m))) ⇒ (||f x - f y|| ≤ (r(n) * r/r(m))))))
BY
{ (InstLemma `implies-isometry-lemma3` []
   THEN RepeatFor 3 (ParallelLast')
   THEN RepeatFor 2 (((D 0 THENA Auto) THEN ThinTrivial))
   THEN 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))
⊢ ||f x - f y|| ≤ (r(n) * r/r(m))

---

Latex:

---

Latex:
No  Annotations
\mforall{}rv:InnerProductSpace.  \mforall{}f:Point(rv)  {}\mrightarrow{}  Point(rv).  \mforall{}r:\{r:\mBbbR{}|  r0  <  r\}  .
    ((\mforall{}x,y:Point(rv).    (x  \mequiv{}  y  {}\mRightarrow{}  f  x  \mequiv{}  f  y))
    {}\mRightarrow{}  (\mforall{}x,y:Point(rv).
                (((||x  -  y||  =  r)  \mvee{}  (||x  -  y||  =  (r(2)  *  r)))  {}\mRightarrow{}  (||f  x  -  f  y||  =  ||x  -  y||)))
    {}\mRightarrow{}  (\mforall{}n,m:\mBbbN{}\msupplus{}.  \mforall{}x,y:Point(rv).
                ((||x  -  y||  <  (r(n)  *  r/r(m)))  {}\mRightarrow{}  (||f  x  -  f  y||  \mleq{}  (r(n)  *  r/r(m))))))


By

---

Latex:
(InstLemma  `implies-isometry-lemma3`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  RepeatFor  2  (((D  0  THENA  Auto)  THEN  ThinTrivial))
  THEN  Auto)

---

Home Index