---

Step * of Lemma Cauchy-Schwarz-strict

∀n:ℕ. ∀x,y:ℝ^n.  (∃i,j:ℕn. (x j) * (y i) ≠ (x i) * (y j) ⇐⇒ |x⋅y| < (||x|| * ||y||))
BY
{ (InstLemma `Cauchy-Schwarz3-strict` []
   THEN RepeatFor 3 ((ParallelLast' THENA Auto))
   THEN Unfold `so_apply` -1
   THEN Fold `dot-product` (-1)
   THEN Fold `real-vec-norm` (-1)
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}x,y:\mBbbR{}\^{}n.    (\mexists{}i,j:\mBbbN{}n.  (x  j)  *  (y  i)  \mneq{}  (x  i)  *  (y  j)  \mLeftarrow{}{}\mRightarrow{}  |x\mcdot{}y|  <  (||x||  *  ||y||))


By

---

Latex:
(InstLemma  `Cauchy-Schwarz3-strict`  []
  THEN  RepeatFor  3  ((ParallelLast'  THENA  Auto))
  THEN  Unfold  `so\_apply`  -1
  THEN  Fold  `dot-product`  (-1)
  THEN  Fold  `real-vec-norm`  (-1)
  THEN  Trivial)

---

Home Index