---

Step * of Lemma real-vec-norm-mul

∀[n:ℕ]. ∀[x:ℝ^n]. ∀[a:ℝ].  (||a*x|| = (|a| * ||x||))
BY
{ (Auto
   THEN (InstLemma `rnexp-req-iff` [⌜2⌝]⋅ THENA Auto)
   THEN BHyp -1 
   THEN Auto
   THEN Thin (-1)
   THEN (RWW "real-vec-norm-squared" 0⋅ THENA Auto)) }

1
1. n : ℕ
2. x : ℝ^n
3. a : ℝ
⊢ a*x⋅a*x = |a| * ||x||^2

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[x:\mBbbR{}\^{}n].  \mforall{}[a:\mBbbR{}].    (||a*x||  =  (|a|  *  ||x||))


By

---

Latex:
(Auto
  THEN  (InstLemma  `rnexp-req-iff`  [\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  BHyp  -1 
  THEN  Auto
  THEN  Thin  (-1)
  THEN  (RWW  "real-vec-norm-squared"  0\mcdot{}  THENA  Auto))

---

Home Index