---

Step * of Lemma Cauchy-Schwarz

∀[n:ℕ]. ∀[x,y:ℝ^n].  (|x ⋅ y| ≤ (||x|| * ||y||))
BY
{ (InstLemma `Cauchy-Schwarz3` []
   THEN RepeatFor 3 (ParallelLast')
   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].    (|x  \mcdot{}  y|  \mleq{}  (||x||  *  ||y||))


By

---

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

---

Home Index