---

Step * of Lemma real-vec-norm-1-exists

No Annotations
∀[n:ℕ+]. ∃b:ℝ^n. (||b|| = r1)
BY
{ (Auto
   THEN D 0 With ⌜λi.if (i =z 0) then r1 else r0 fi ⌝ 
   THEN Auto
   THEN RepUR ``real-vec-norm`` 0
   THEN BLemma `implies-rsqrt-is-one`
   THEN Auto
   THEN RepUR ``dot-product`` 0) }

1
1. n : ℕ+
⊢ Σ{if (i =z 0) then r1 else r0 fi  * if (i =z 0) then r1 else r0 fi  | 0≤i≤n - 1} = r1

---

Latex:

---

Latex:
No  Annotations
\mforall{}[n:\mBbbN{}\msupplus{}].  \mexists{}b:\mBbbR{}\^{}n.  (||b||  =  r1)


By

---

Latex:
(Auto
  THEN  D  0  With  \mkleeneopen{}\mlambda{}i.if  (i  =\msubz{}  0)  then  r1  else  r0  fi  \mkleeneclose{} 
  THEN  Auto
  THEN  RepUR  ``real-vec-norm``  0
  THEN  BLemma  `implies-rsqrt-is-one`
  THEN  Auto
  THEN  RepUR  ``dot-product``  0)

---

Home Index