---

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


1. rv : InnerProductSpace
2. m : ℕ+
3. y : Point(rv)
4. x : Point(rv)
5. s : ℝ
6. r0 < s
7. ||y - x|| = s
8. xx + r(m)*y - x=xx + r(m)*y - x
⊢ ||y - x + r(m)*y - x|| ≤ ||y - y + r(m)*x - y||
BY
{ ((Assert y - y + r(m)*x - y ≡ r(-m)*x - y BY
          (RealVecEqual THEN Auto))
   THEN RWW   "-1 rv-norm-mul" 0
   THEN Auto
   THEN (Assert y - x + r(m)*y - x ≡ r(m - 1)*x - y BY
               (RealVecEqual THEN Auto))
   THEN RWW   "-1 rv-norm-mul" 0
   THEN Auto) }

1
1. rv : InnerProductSpace
2. m : ℕ+
3. y : Point(rv)
4. x : Point(rv)
5. s : ℝ
6. r0 < s
7. ||y - x|| = 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.  y  :  Point(rv)
4.  x  :  Point(rv)
5.  s  :  \mBbbR{}
6.  r0  <  s
7.  ||y  -  x||  =  s
8.  xx  +  r(m)*y  -  x=xx  +  r(m)*y  -  x
\mvdash{}  ||y  -  x  +  r(m)*y  -  x||  \mleq{}  ||y  -  y  +  r(m)*x  -  y||


By

---

Latex:
((Assert  y  -  y  +  r(m)*x  -  y  \mequiv{}  r(-m)*x  -  y  BY
                (RealVecEqual  THEN  Auto))
  THEN  RWW      "-1  rv-norm-mul"  0
  THEN  Auto
  THEN  (Assert  y  -  x  +  r(m)*y  -  x  \mequiv{}  r(m  -  1)*x  -  y  BY
                          (RealVecEqual  THEN  Auto))
  THEN  RWW      "-1  rv-norm-mul"  0
  THEN  Auto)

---

Home Index