---

Step * of Lemma real-vec-norm-diff

∀[n:ℕ]. ∀[x,y:ℝ^n].  (||x - y|| = ||y - x||)
BY
{ (Auto
   THEN (Assert req-vec(n;y - x;r(-1)*x - y) BY
               ((D 0 THENA Auto) THEN RepUR ``real-vec-mul real-vec-sub`` 0 THEN nRNorm 0 THEN Auto))
   ) }

1
1. n : ℕ
2. x : ℝ^n
3. y : ℝ^n
4. req-vec(n;y - x;r(-1)*x - y)
⊢ ||x - y|| = ||y - x||

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[x,y:\mBbbR{}\^{}n].    (||x  -  y||  =  ||y  -  x||)


By

---

Latex:
(Auto
  THEN  (Assert  req-vec(n;y  -  x;r(-1)*x  -  y)  BY
                          ((D  0  THENA  Auto)  THEN  RepUR  ``real-vec-mul  real-vec-sub``  0  THEN  nRNorm  0  THEN  Auto))
  )

---

Home Index