---

Step * 1 of Lemma real-vec-infinity-norm-req


1. n : ℕ+
2. v : ℝ^n
⊢ ||v||∞ = if (n =z 1) then |v 0| else rmax(||v||∞;|v (n - 1)|) fi 
BY
{ RepUR ``real-vec-infinity-norm mdist max-metric`` 0 }

1
1. n : ℕ+
2. v : ℝ^n
⊢ primrec(n;r0;λi,r. rmax(r;|(v i) - r0|))
= if (n =z 1) then |v 0| else rmax(primrec(n - 1;r0;λi,r. rmax(r;|(v i) - r0|));|v (n - 1)|) fi 

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  v  :  \mBbbR{}\^{}n
\mvdash{}  ||v||\minfty{}  =  if  (n  =\msubz{}  1)  then  |v  0|  else  rmax(||v||\minfty{};|v  (n  -  1)|)  fi 


By

---

Latex:
RepUR  ``real-vec-infinity-norm  mdist  max-metric``  0

---

Home Index