---

Step * of Lemma real-vec-norm-diff-squared

∀[n:ℕ]. ∀[x,y:ℝ^n].  (||x - y||^2 = ((||x||^2 + ||y||^2) + (r(-2) * x⋅y)))
BY
{ (Auto THEN (RWW "real-vec-norm-squared dot-product-linearity1-sub.1 dot-product-linearity1-sub.2" 0  THENA Auto)) }

1
1. n : ℕ
2. x : ℝ^n
3. y : ℝ^n
⊢ (x⋅x - x⋅y - y⋅x - y⋅y) = ((x⋅x + y⋅y) + (r(-2) * x⋅y))

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (RWW  "real-vec-norm-squared  dot-product-linearity1-sub.1  dot-product-linearity1-sub.2"  0 
              THENA  Auto
              )
  )

---

Home Index