---

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


1. rv : InnerProductSpace
2. m : ℕ+
3. x : Point(rv)
4. y : Point(rv)
5. s : ℝ
6. r0 < s
7. ||x - y|| = s
8. xx + r(m)*y - x=xx + r(m)*y - x
9. y - y + r(m)*x - y ≡ r(-m)*x - y
10. y - x + r(m)*y - x ≡ r(m - 1)*x - y
⊢ (|r(m - 1)| * ||x - y||) ≤ (|r(-m)| * ||x - y||)
BY
{ (RWW "rabs-int absval-minus" 0 THENA Auto) }

1
1. rv : InnerProductSpace
2. m : ℕ+
3. x : Point(rv)
4. y : Point(rv)
5. s : ℝ
6. r0 < s
7. ||x - y|| = s
8. xx + r(m)*y - x=xx + r(m)*y - x
9. y - y + r(m)*x - y ≡ r(-m)*x - y
10. y - x + r(m)*y - x ≡ r(m - 1)*x - y
⊢ (r(|m - 1|) * ||x - y||) ≤ (r(|m|) * ||x - y||)

---

Latex:

---

Latex:

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
8.  xx  +  r(m)*y  -  x=xx  +  r(m)*y  -  x
9.  y  -  y  +  r(m)*x  -  y  \mequiv{}  r(-m)*x  -  y
10.  y  -  x  +  r(m)*y  -  x  \mequiv{}  r(m  -  1)*x  -  y
\mvdash{}  (|r(m  -  1)|  *  ||x  -  y||)  \mleq{}  (|r(-m)|  *  ||x  -  y||)


By

---

Latex:
(RWW  "rabs-int  absval-minus"  0  THENA  Auto)

---

Home Index