---

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


1. rv : InnerProductSpace
2. y : Point(rv)
3. z : Point(rv)
4. v : ℝ
5. r0 < v
⊢ y ≡ z + v*z + (r1/v)*y - z - z
BY
{ (RealVecEqual THEN Auto) }

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  y  :  Point(rv)
3.  z  :  Point(rv)
4.  v  :  \mBbbR{}
5.  r0  <  v
\mvdash{}  y  \mequiv{}  z  +  v*z  +  (r1/v)*y  -  z  -  z


By

---

Latex:
(RealVecEqual  THEN  Auto)

---

Home Index