---

Step * of Lemma implies-isometry

∀rv:InnerProductSpace. ∀f:Point ⟶ Point. ∀r:{r:ℝ| r0 < r} . ∀N:{2...}.
  ((∀x,y:Point.  (x ≡ y ⇒ f x ≡ f y))
  ⇒ (∀x,y:Point.  ((||x - y|| = r) ⇒ (||f x - f y|| ≤ r)))
  ⇒ (∀x,y:Point.  ((||x - y|| = (r(N) * r)) ⇒ ((r(N) * r) ≤ ||f x - f y||)))
  ⇒ is-isometry(rv;f))
BY
{ (InstLemma `implies-isometry-lemma1` [] THEN RepeatFor 7 ((ParallelLast' THENA Auto)) THEN Unfold `guard` -1) }

1
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||))
⊢ is-isometry(rv;f)

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}f:Point  {}\mrightarrow{}  Point.  \mforall{}r:\{r:\mBbbR{}|  r0  <  r\}  .  \mforall{}N:\{2...\}.
    ((\mforall{}x,y:Point.    (x  \mequiv{}  y  {}\mRightarrow{}  f  x  \mequiv{}  f  y))
    {}\mRightarrow{}  (\mforall{}x,y:Point.    ((||x  -  y||  =  r)  {}\mRightarrow{}  (||f  x  -  f  y||  \mleq{}  r)))
    {}\mRightarrow{}  (\mforall{}x,y:Point.    ((||x  -  y||  =  (r(N)  *  r))  {}\mRightarrow{}  ((r(N)  *  r)  \mleq{}  ||f  x  -  f  y||)))
    {}\mRightarrow{}  is-isometry(rv;f))


By

---

Latex:
(InstLemma  `implies-isometry-lemma1`  []
  THEN  RepeatFor  7  ((ParallelLast'  THENA  Auto))
  THEN  Unfold  `guard`  -1)

---

Home Index