---

Step * 1 of Lemma punit-norm1


1. n : ℕ
2. a : ℙ^n
⊢ ||u(a)|| = r1
BY
{ (RepUR ``punit`` 0 THEN RWO "real-vec-norm-mul" 0 THEN Auto) }

1
1. n : ℕ
2. a : ℙ^n
⊢ (|(r1/||a||)| * ||a||) = r1

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  a  :  \mBbbP{}\^{}n
\mvdash{}  ||u(a)||  =  r1


By

---

Latex:
(RepUR  ``punit``  0  THEN  RWO  "real-vec-norm-mul"  0  THEN  Auto)

---

Home Index