---

Step * 1 of Lemma rleq-real-vec-dist


1. n : ℕ
2. x : ℝ^n
3. y : ℝ^n
4. i : ℕn
⊢ (((x i) - y i) * ((x i) - y i)) ≤ x - y⋅x - y
BY
{ (RepUR ``dot-product`` 0
   THEN InstLemma `item-rleq-rsum-of-nonneg` [⌜0⌝;⌜n - 1⌝;⌜λ2i.(x - y i) * (x - y i)⌝;⌜i⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  x  :  \mBbbR{}\^{}n
3.  y  :  \mBbbR{}\^{}n
4.  i  :  \mBbbN{}n
\mvdash{}  (((x  i)  -  y  i)  *  ((x  i)  -  y  i))  \mleq{}  x  -  y\mcdot{}x  -  y


By

---

Latex:
(RepUR  ``dot-product``  0
  THEN  InstLemma  `item-rleq-rsum-of-nonneg`  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}n  -  1\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}i.(x  -  y  i)  *  (x  -  y  i)\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index