---

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

.....set predicate..... 
1. rv : InnerProductSpace
2. m : ℕ+
3. x : Point(rv)
4. y : Point(rv)
5. s : ℝ
6. r0 < s
7. ||x - y|| = s
⊢ x # y
BY
{ EAuto 1 }

---

Latex:

---

Latex:
.....set  predicate..... 
1.  rv  :  InnerProductSpace
2.  m  :  \mBbbN{}\msupplus{}
3.  x  :  Point(rv)
4.  y  :  Point(rv)
5.  s  :  \mBbbR{}
6.  r0  <  s
7.  ||x  -  y||  =  s
\mvdash{}  x  \#  y


By

---

Latex:
EAuto  1

---

Home Index